[isabelle] Locale internal assumptions



Hi all,

I'm looking at expression.ML and at fun eval_text, the comment above mentions

(* ... ints: internal assumptions (terms in assumptions from insts)...*)

What are "insts"? Instantiations? Or simply, what are internal assumptions and how are they represented in Isar?

Thank you

Steve




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.