If you do these things, you put an end to all Isabelle logics other than Isabelle/HOL. Remember, an object logic does not need to possess an equality symbol or even an implication symbol.
Having just translated some lengthy, incomprehensible HOL proofs into Isabelle, I appreciate more than ever the distinction between the meta- and object- levels. HOL proofs are cluttered with extra steps to manipulate implications because HOL has no other way to express the dependence of a fact upon conditions. Larry On 11 Nov 2009, at 23:22, Brian Huffman wrote: > Anyway, since eq_reflection actually *is* an axiom, and (=) actually > *does* mean the same thing as (==), then I really don't see any reason > why we need to have both (or separate bool and prop types, for that > matter). I don't know of any other HOL provers that do. > > Even if we got rid of the bool/prop and (=)/(==) distinctions, we > still have the "meta-meta-logic" as a natural deduction framework: The > "hyps" component of theorems encodes the "is derivable from" relation, > and free variables in theorems encode the "this derivation can be done > uniformly for all x" property. I have never understood why Isabelle > needs multiple levels of meta-logics.