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

[Jasmin Christian Blanchette]

Am 13.11.2009 um 10:07 schrieb 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?

I'm not sure this is the right analogy; after all, your retorical  
question, in the original context of !! and ==>, can be answered by  
"the HOL4 and HOL Light developers." Isabelle's metalogic, just like  
and/or/not/implies, is extracting a certain price, and some of the  
people paying that price are wondering what they get for their money.  
If nothing else, this discussion was very informative.

Jasmin