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

[Lawrence Paulson]

The situation regarding these inference rules is quite different.  
Isabelle is primarily based on resolution, which is a big, complicated  
piece of code implementing what is supposed to be a sound form of  
reasoning in intuitionistic Higher-order logic. However, it claims to  
be based on that logic and therefore I included the corresponding  
presentation in the form of LCF-style inference rules. They were  
almost never used, and very annoyingly, somebody once identified a bug  
in one that could break the type system!

It was obvious to me from the start that there were some redundancy  
between the built-in resolution code and these rules, but I never saw  
this issue as a priority.
Larry

On 11 Nov 2009, at 23:22, Brian Huffman wrote:

> (Actually, it is slightly more complicated than that, since there is a
> primitive inference rule Thm.equal_intr that makes (==) at type prop
> the same as bi-implication. I don't really see why equal_intr needs to
> exist at all; maybe just to make simplification easier? Oh, well.)