Hi Lars, > in 40fe6b80b481, I stumbled upon the following behaviour. Consider > the following example: > > locale Foo = fixes a :: 'a > > notepad begin > interpret Foo b for b . > term b > end > > jEdit tells me about b in the term command: > > term > fixed "b" > skolem variable > :: 'b > > So the b from the "for b" is leaked into the surrounding context. As all > the lemmas about b where generalized, I would have expected that > b does not become fixed in the surrounding context.
I guess the for-parameters are not dealt as expected by interpret.
Maybe this is a co-phenomenon of the following warning from isar-ref:
> interpret expr where eqns interprets expr in the proof context and is
> otherwise similar to interpretation in local theories. Note that rewrite
> rules given to interpret after the where keyword should be explicitly
> universally quantified.
Cheers,
Florian Haftmann
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
