[isabelle-dev] Isabelle/HOL axiom ext is redundant

Lawrence Paulson lp15 at cam.ac.uk
Fri Nov 13 10:07:01 CET 2009

This sort of discussion is analogous to suggesting that we get rid of  
and/or/not/implies and write all formulas using the Scheffer stroke  
(NAND), or that Gentzen's sequent calculus should be replaced by the  
much simpler Hilbert system. It can be done, but who would want to do  


On 12 Nov 2009, at 20:50, Lucas Dixon wrote:

> this is interesting to me: I don't understand why you couldn't just  
> use
> the --> and ALL of HOL to do exactly what ==> and !! are doing? Isn't
> that what SPL by Zammit did? The dependencies (in Isabelle, stored in
> hyps) can all be recorded outside the logic (as they are in SPL). If
> done correctly, like Isar, the final theorems can be re-constructed
> easily enough from the recorded structure of the proof text... or so  
> it
> seems to me. :)

More information about the isabelle-dev mailing list