Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Locale internal assumptions

view this post on Zulip Email Gateway (Aug 18 2022 at 16:53):

From: Clemens Ballarin <ballarin@in.tum.de>
Quoting s.wong.731@gmail.com:

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

view this post on Zulip Email Gateway (Aug 18 2022 at 16:59):

From: s.wong.731@gmail.com
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

Last updated: Apr 19 2024 at 16:20 UTC