Re: [isabelle] Locale internal assumptions



Quoting s.wong.731 at gmail.com:

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.

Clemens






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