Re: [isabelle] Locale internal assumptions

Quoting s.wong.731 at

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?

Insts is usually used to denote locale instances. Internal assumptions are those that have already been internalised. This means that they stem from the imported locale expression, and they always involve locale predicates. The external assumptions are from the assumes elements of the locale declaration.


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