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