Thanks for this interesting and enlightening discussion. I have always had an intuitive appreciation of the meta-logic in Isabelle. I find it clarifies the both the modeling and proof activities profoundly.
I would be interested also in a discussion of an important place where the meta-logic is not distinguished from the object logic in Isabelle/ HOL, i.e. in the function model. HOL functions are completely identified with meta-functions (I like to call them operators) and there is no explicit function application operator. This makes for lots of inconvenience in making proofs about HOL functions, especially in the vagaries higher-order unification. Any insights in why HOL-application is not as worthy of distinction from meta-application as = is from ==? Especially as meta-application itself is so subtly identified with term construction? On 13/11/2009, at 5:36 AM, Brian Huffman wrote: > Right, having two kinds of implication (--> and ==>) is convenient > because (==>) is used to encode subgoals with premises in apply-style > Isabelle proofs. IMPORTANT: This email remains the property of the Australian Defence Organisation and is subject to the jurisdiction of section 70 of the CRIMES ACT 1914. If you have received this email in error, you are requested to contact the sender and delete the email.