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

[Lawrence Paulson]

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  
it?

Larry

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. :)