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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and