Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Towards localized syntax: bundle mixins f...

view this post on Zulip Email Gateway (Nov 21 2020 at 08:01):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Since this thread did not stimulate any activity I will go on to
document the syntax in NEWS entries and manuals.

Cheers,
Florian
signature.asc

view this post on Zulip Email Gateway (Nov 27 2020 at 17:46):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
See now http://isabelle.in.tum.de/repos/isabelle/rev/e7c2848b78e8 for a
refined and documented version.

Florian
signature.asc

view this post on Zulip Email Gateway (Dec 03 2020 at 20:35):

From: Clemens Ballarin <ballarin@in.tum.de>
Hi Florian,

Could you please explain what you mean by "surface context" in the
documentation of the locale command:

isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev

view this post on Zulip Email Gateway (Dec 04 2020 at 14:11):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Clemens,

exactly. The surface context is the epheneral hypothetical context on
top of the local theory stack without any permanent effect.

Hope this helps,
Florian
signature.asc

Last updated: Dec 07 2024 at 16:22 UTC