Re: [isabelle-dev] Interpretation in arbitrary targets.
On 21.05.2013 13:59, Makarius wrote: I do this usually by searching backwards for context (which means I might miss contexts opened by locale) or manually search through the sidekick. To check whether I am in a local context at all, I usually insert an additional end command and look for an error. BTW, there is also the old-fashioned TTY command print_context to ask the prover. It is more relevant in non-trivial contexts like 'interpretation'. On the other hand, all these things should be more immediate in the Prover IDE, as generated templates or similar. I did not know about print_context, which solves my immediate use case. This command is not documented in the reference manual (at least not in the index), though. Also, it only seems to work half-way for unnamed contexts: - If I open an unnamed context with some fixes, assumes in the theory context, print_context ignores this, i.e. in theory Foo imports Main begin context fixes P assumes P begin print_context outputs only theory Foo. - This is different inside a named context: theory Foo imports Main begin locale A begin context fixes P assumes P begin yields theory Foo locale A = fixes P :: bool assumes P as output of print_context. Although this might also be considered slightly irritating, as those elements are not part of the locale, so something like theory Foo locale A context fixes P :: bool assumes P would be better. How is interpretation related to print_context? It seems that neither interpret nor interpretation extends the context as displayed by print_context? -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
On 23.04.2013 19:37, Florian Haftmann wrote:
See now http://isabelle.in.tum.de/repos/isabelle/rev/e4b5bebe5235.
This does not seem to work for me in 06db08182c4b:
-
theory Interpretation imports Main begin
locale A begin
definition f :: bool where f ≡ True
end
context begin
interpretation I: A by unfold_locales
thm I.f_def (* Unknown fact I.f_def *)
end
interpretation I: A by unfold_locales
thm I.f_def (* Works *)
-
It seems that the interpretation inside the context block has no effect
at all?
When following the suggestions of the ML code
http://isabelle.in.tum.de/repos/isabelle/file/9e4220605179/src/Pure/Isar/expression.ML#l42
I am personally still in favor of only three Isar keywords, corresponding to
permanent_interpretation
ephemeral_interpretation
interpret
with the perspective to generalize permanent_interpretation from named
targets to arbitrary targets by means of a dedicated local theory
operation, like Local_Theory.subscription in the previous series of
patches. But for the moment I will leave this aside anyway.
I don't know whether this is what you are talking about, but there is
one functionality I would like to have for my Graph theory:
I have a locale (or rather, a locale hierarchy) describing a single
graph. I chose this formalization as I usually talk about a single
graph. However, if I want to talk about multiple graphs (for example
because I want to prove properties of union) it would be nice to
switch to a mode of working as in HOL-Algebra (i.e. have an explicit
domain and all lemmas only hold for elements of the domain).
It seems with your suggestion above, I could do something like
--
locale graphs =
defines GG = {G. graph G}
begin
context
fixes G assumes G : GG
begin
permanent_interpretation graph G sorry
end
--
to get all the lemmas of graph in graph, with the additional assumption
G : GG. Of course, one would need to transfer the automation manually,
as in particular elim and dest are not stable under such a transformation.
-- Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
Quoting Lars Noschinski nosch...@in.tum.de: How is interpretation related to print_context? It seems that neither interpret nor interpretation extends the context as displayed by print_context? I don't know the answer to that, but for a particular locale x you should be able to find all active interpretations in a context by print_interps x Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
On Wed, 17 Apr 2013, Clemens Ballarin wrote: Quoting Makarius makar...@sketis.net: That is just a matter of modularity of concepts: the older (in a) notation was slightly generalized at some point to allow named contexts as sketched above In any case, I'm not sure how useful the old notation still is. Maybe it can be given up at some point. (Clearing out old mail threads, I've come across this again.) Does it mean you propose to discontinue (in a) at some point? An old idea on my list is to add some support to the Prover IDE to rework theories with many consecutive (in a) to use just one context a begin ... end around it -- this is also more efficient. Apart from that I have occasionally considered to provide explicit fold support for such contexts in the editor -- the canonical layout does not have any indentation here. Thus (in a) would eventually become more rare in practice, although my speculations did not go as far as discontinuing it altogether. It might be worth to reconsider that question at some point nonetheless. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
Naturally this notation is less important than before, and never strictly essential. But would we save much by eliminating it? Larry On 21 May 2013, at 11:46, Makarius makar...@sketis.net wrote: Does it mean you propose to discontinue (in a) at some point? An old idea on my list is to add some support to the Prover IDE to rework theories with many consecutive (in a) to use just one context a begin ... end around it -- this is also more efficient. Apart from that I have occasionally considered to provide explicit fold support for such contexts in the editor -- the canonical layout does not have any indentation here. Thus (in a) would eventually become more rare in practice, although my speculations did not go as far as discontinuing it altogether. It might be worth to reconsider that question at some point nonetheless. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
On 21.05.2013 12:46, Makarius wrote: An old idea on my list is to add some support to the Prover IDE to rework theories with many consecutive (in a) to use just one context a begin ... end around it -- this is also more efficient. Apart from that I have occasionally considered to provide explicit fold support for such contexts in the editor -- the canonical layout does not have any indentation here. I don't know whether context blocks are an important unit for folding, but something I have missed recently is a quick way to find out in what context I am at a certain point in my theory. I do this usually by searching backwards for context (which means I might miss contexts opened by locale) or manually search through the sidekick. To check whether I am in a local context at all, I usually insert an additional end command and look for an error. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
On Tue, 21 May 2013, Lars Noschinski wrote: On 21.05.2013 12:46, Makarius wrote: An old idea on my list is to add some support to the Prover IDE to rework theories with many consecutive (in a) to use just one context a begin ... end around it -- this is also more efficient. Apart from that I have occasionally considered to provide explicit fold support for such contexts in the editor -- the canonical layout does not have any indentation here. I don't know whether context blocks are an important unit for folding, but something I have missed recently is a quick way to find out in what context I am at a certain point in my theory. OK, that's part of some first-class support of logical contexts within the editor. I am reminded about the lack of something like that everytime I see funny comments like that: context foo begin ... end (* context foo *) Luckily such formally unchecked comments are rare. I do this usually by searching backwards for context (which means I might miss contexts opened by locale) or manually search through the sidekick. To check whether I am in a local context at all, I usually insert an additional end command and look for an error. BTW, there is also the old-fashioned TTY command print_context to ask the prover. It is more relevant in non-trivial contexts like 'interpretation'. On the other hand, all these things should be more immediate in the Prover IDE, as generated templates or similar. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
Quoting Makarius makar...@sketis.net: Does it mean you propose to discontinue (in a) at some point? Exactly. Too early right now, but eventually this might make sense -- especially if the IDE provides suitable refactorings. Of course, this wouldn't let us scrap a lot of code, but the Isar language could become cleaner. Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
But for the moment I will leave this aside anyway. Still one thing to add: http://isabelle.in.tum.de/repos/isabelle/rev/cb154917a496 avoids the odd reinit entirely, the critical lines being fun add_dependency locale dep_morph mixin export = (Local_Theory.raw_theory ooo Locale.add_dependency locale) dep_morph mixin export # activate_local_theory dep_morph mixin export which add both an dependency *and* provide the facts in the context of the current local theory. Also, interpretation confined within blocks essentially boils down to the singleton line val activate_local_theory = Local_Theory.target ooo activate_proof; This is a great triumph of the »local everything« approach. Florian -- 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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
Hi, Am Mittwoch, den 24.04.2013, 19:16 +0200 schrieb Florian Haftmann: This is a great triumph of the »local everything« approach. I’m not sure that I understand all that is going on, but I have the feeling that the theory that I’m working on will greatly benefit from your development, and I’m looking forward to Isabelle 2013-2 (or 2014). So thanks in advance from my side! Greetings, Joachim -- Dipl.-Math. Dipl.-Inform. Joachim Breitner Wissenschaftlicher Mitarbeiter http://pp.ipd.kit.edu/~breitner signature.asc Description: This is a digitally signed message part ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
See now http://isabelle.in.tum.de/repos/isabelle/rev/e4b5bebe5235. When following the suggestions of the ML code http://isabelle.in.tum.de/repos/isabelle/file/9e4220605179/src/Pure/Isar/expression.ML#l42 I am personally still in favor of only three Isar keywords, corresponding to permanent_interpretation ephemeral_interpretation interpret with the perspective to generalize permanent_interpretation from named targets to arbitrary targets by means of a dedicated local theory operation, like Local_Theory.subscription in the previous series of patches. But for the moment I will leave this aside anyway. Cheers, Florian -- 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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
Hi Clemens, Please let me know if you need to make changes to locales.ML. I want to make sure that routes out of certain quirks there don't get blocked accidentally. the only change to locales.ML in the pipeline is http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/21821401c5a5 and I do not forsee anything else in that respect. If it comes to happen nonetheless, I will exhibit that change similarly before pushing it to any main upstream. Florian -- 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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
Let me just make some remarks as a user. At ITP 2011 I published a paper http://www21.in.tum.de/~nipkow/pubs/itp11.html where I showed how to use locales to structure stepwise development of modules (see p11). In that context I intentionally used the notation interpretation (in A) B-expr instead of sublocale in an implementation step. Of course I comment on the deviation in the notation saying that I have chosen this variation of interpretation because it is more intuitive (see p10). I do find it more intuitive because it tells me clearly what is going on: some locale expression is interpreted in some locale. And this is also how you explain sublocale in your locale tutorial. Hence Florian's suggestions made a lot of sense to me. Tobias Am 17/04/2013 22:28, schrieb Clemens Ballarin: Quoting Makarius makar...@sketis.net: On Fri, 12 Apr 2013, Clemens Ballarin wrote: That sounds a bit dogmatic. If additional commands are made available for targets, then the syntax should clearly be more flexible if better intuition can be achieved. That is just a matter of modularity of concepts: the older (in a) notation was slightly generalized at some point to allow named contexts as sketched above, and the relation between the two is as pointed out by Florian. I am aware of the modularity aspect of this. My criticism is that deviations from the current approach in favour of preferable notation are not even considered. In any case, I'm not sure how useful the old notation still is. Maybe it can be given up at some point. Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
Hi Clemens, I still see us disagree on how far the local theory game can be driven wrt. interpretation, nevertheless I can imagine that there is an intermediate road map which we can agree on: * Extend sublocale for use within locale targets s.t. This is fine with me. Will this work for named targets including classes or just locales? it will work within locales, and thus within type classes. * Equip interpretation in non-theory targets to allow confined, non-persistent interpretations. context B begin interpretation EXPR end would not add a dependency to B. Here, it's not clear whether the interpretation just wouldn't add a dependency, or wouldn't modify B at all. It should not modify B at all -- with the restriction that ad-hoc contexts currently may leak nontheless in certain situations (cf. Makarius' statement). Florian -- 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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
Hi Florian, OK, then we agree on this. Please let me know if you need to make changes to locales.ML. I want to make sure that routes out of certain quirks there don't get blocked accidentally. Clemens Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de: Hi Clemens, I still see us disagree on how far the local theory game can be driven wrt. interpretation, nevertheless I can imagine that there is an intermediate road map which we can agree on: * Extend sublocale for use within locale targets s.t. This is fine with me. Will this work for named targets including classes or just locales? it will work within locales, and thus within type classes. * Equip interpretation in non-theory targets to allow confined, non-persistent interpretations. context B begin interpretation EXPR end would not add a dependency to B. Here, it's not clear whether the interpretation just wouldn't add a dependency, or wouldn't modify B at all. It should not modify B at all -- with the restriction that ad-hoc contexts currently may leak nontheless in certain situations (cf. Makarius' statement). Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
This view is correct, but it is not the whole story. Since the system maintains a graph of interpretations and follows them transitively, the effect achieved by sublocale locale expression is much like instance class sort of the old user interface to type classes. This relationship is discussed in the new paper (Section 5.2). Clemens Quoting Tobias Nipkow nip...@in.tum.de: Let me just make some remarks as a user. At ITP 2011 I published a paper http://www21.in.tum.de/~nipkow/pubs/itp11.html where I showed how to use locales to structure stepwise development of modules (see p11). In that context I intentionally used the notation interpretation (in A) B-expr instead of sublocale in an implementation step. Of course I comment on the deviation in the notation saying that I have chosen this variation of interpretation because it is more intuitive (see p10). I do find it more intuitive because it tells me clearly what is going on: some locale expression is interpreted in some locale. And this is also how you explain sublocale in your locale tutorial. Hence Florian's suggestions made a lot of sense to me. Tobias Am 17/04/2013 22:28, schrieb Clemens Ballarin: Quoting Makarius makar...@sketis.net: On Fri, 12 Apr 2013, Clemens Ballarin wrote: That sounds a bit dogmatic. If additional commands are made available for targets, then the syntax should clearly be more flexible if better intuition can be achieved. That is just a matter of modularity of concepts: the older (in a) notation was slightly generalized at some point to allow named contexts as sketched above, and the relation between the two is as pointed out by Florian. I am aware of the modularity aspect of this. My criticism is that deviations from the current approach in favour of preferable notation are not even considered. In any case, I'm not sure how useful the old notation still is. Maybe it can be given up at some point. Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
Hi Florian, I still see us disagree on how far the local theory game can be driven wrt. interpretation, nevertheless I can imagine that there is an intermediate road map which we can agree on: * Extend sublocale for use within locale targets s.t. This is fine with me. Will this work for named targets including classes or just locales? Rationale: We have 30 occurences of sublocale in HOL/*.thy and 80% and more occur with the pattern That's not very much. In any case, in future, I would prefer a discussion starting from the problem towards a solution, not from a solution to the actual problem. * Equip interpretation in non-theory targets to allow confined, non-persistent interpretations. context B begin interpretation EXPR end would not add a dependency to B. Here, it's not clear whether the interpretation just wouldn't add a dependency, or wouldn't modify B at all. Please clarify. Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
Quoting Makarius makar...@sketis.net: On Fri, 12 Apr 2013, Clemens Ballarin wrote: That sounds a bit dogmatic. If additional commands are made available for targets, then the syntax should clearly be more flexible if better intuition can be achieved. That is just a matter of modularity of concepts: the older (in a) notation was slightly generalized at some point to allow named contexts as sketched above, and the relation between the two is as pointed out by Florian. I am aware of the modularity aspect of this. My criticism is that deviations from the current approach in favour of preferable notation are not even considered. In any case, I'm not sure how useful the old notation still is. Maybe it can be given up at some point. Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
Hi Clemens, I hope, though, it has become clear that I'm not opposed to having interpretation in locale contexts by principle, I'm merely opposed to explaining them in the way you propose. I still see us disagree on how far the local theory game can be driven wrt. interpretation, nevertheless I can imagine that there is an intermediate road map which we can agree on: * Extend sublocale for use within locale targets s.t. context B begin sublocale EXPR end is equivalent to sublocale B EXPR Rationale: We have 30 occurences of sublocale in HOL/*.thy and 80% and more occur with the pattern context B begin … end sublocale B EXPR context B begin … end * Equip interpretation in non-theory targets to allow confined, non-persistent interpretations. context B begin interpretation EXPR end would not add a dependency to B. Would this make sense? I still think that the frontiers can be pushed further, but this can still be a separate step, on which discussion can be resumed after. Cheers, Florian -- 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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
Hi Florian, I do not object to your suggestion, and it is clearly in reach within the current code base. But... it is a different thing. Your suggestion is to make sublocale work in locale targets seamlessly. But something like instantiation ... begin sublocale ... instance ... end then just does not make sense: either it is not covered (or blocked) by the implementation, or »sublocale« is just the wrong wording since it assumes locales on both producer and consumer side so to speak. I don't know what interpretation (or sublocale) would mean in an instantiation context, so I cannot tell what would be more appropriate. It seems natural though, that, if additional commands are to be 'targetized', some commands will not be meaningful in some kinds of targets. So, if sublocale were only available in locale targets, I wouldn't consider that a problem. (If sublocale were not available in locale targets, I wouldn't consider that a problem either, but that's not the the point of this discussion.) In any case, it would make sense to discuss what a command would mean in all of the targets (and where it is not meaningful) before making it available in some targets. You might ask at first what interpretation in instantiation blocks is supposed to be. I think it can be a neat pattern to approach instantiation by default definitions; here the interpretation would provide that OFCLASS theorem to prove the claimed instance relationship finally or something alike. I'm unsure whether I understand this fully. But to me it looks like the purpose of the instantiation target is to declare instance relations between classes. If that is the case, then there is no further need to stress the 'subscriptive' nature and it might be legitimate to just call the command 'interpretation'. But, of course, it depends on what the command would actually do. I guess this would replace some existing command that already exists. This is different if the target is a locale. The purpose of a locale target is to work in a locale, not add relations between locales. We don't have a sublocale target, whose purpose could be to establish interpretation relations between locales. Instead there is just the sublocale command, which is fairly primitive. The mechanisms offered by the instantiation target, which lets one make the necessary constructions needed for the instantiation in a clean way, are much more elaborate. Two asides: Of course, the global version should remain sublocale l e. It should not be turned into sublocale (in l) e foo (in l) ... is equivalent to context l begin foo ... end by construction. We cannot have just one of them. That sounds a bit dogmatic. If additional commands are made available for targets, then the syntax should clearly be more flexible if better intuition can be achieved. It is also notable that we have definitions in locales (although this is far beneath your great achievements with sublocale etc.). With them it is the case that we provide them *uniformly* for theories, locales and other targets (something which has been commented as seemingly trivial, »but maybe this is the achievement.« ). I strongly believe that definitions in locales are a great achievement. Without them all the other work would not have been worth it. I hope, though, it has become clear that I'm not opposed to having interpretation in locale contexts by principle, I'm merely opposed to explaining them in the way you propose. Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
On Fri, 12 Apr 2013, Clemens Ballarin wrote: foo (in l) ... is equivalent to context l begin foo ... end by construction. We cannot have just one of them. That sounds a bit dogmatic. If additional commands are made available for targets, then the syntax should clearly be more flexible if better intuition can be achieved. That is just a matter of modularity of concepts: the older (in a) notation was slightly generalized at some point to allow named contexts as sketched above, and the relation between the two is as pointed out by Florian. A localized Isar command does not see the difference, since this is managed uniformly by the toplevel. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
Hi Clemens, Let those thoughts sink further few days. If there is no veto until Apr 7th, I would go ahead to turn the patches upstream. You have proposed a change about which doubts were raised. I don't consider it acceptable to then announce a deadline after which you will go ahead and push. People simply may not be able to respond in time, especially in a vacation period. This was by no means meant to put pressure on anybody or you in particular. For this sake I have asked for a »veto« which does not need a justification at the same time. Let me note that, of course, the user interface design should not make the implementation unnecessarily complicated (but I believe we are far away from that). Agree. In this light, if a version of the sublocale command seems necessary in context blocks, why no call it 'sublocale'? Of course, the global version should remain sublocale l e. It should not be turned into sublocale (in l) e because the former much more clearly indicates the change to the locale hierarchy. This design has the additional benefits that users don't need to change existing proof documents, terminology in the literature remains up to date, and, most importantly, the sublocale command is clearly recognisable in context blocks. I do not object to your suggestion, and it is clearly in reach within the current code base. But… it is a different thing. Your suggestion is to make sublocale work in locale targets seamlessly. But something like instantiation … begin sublocale … instance … end then just does not make sense: either it is not covered (or blocked) by the implementation, or »sublocale« is just the wrong wording since it assumes locales on both producer and consumer side so to speak. You might ask at first what interpretation in instantiation blocks is supposed to be. I think it can be a neat pattern to approach instantiation by default definitions; here the interpretation would provide that OFCLASS theorem to prove the claimed instance relationship finally or something alike. Just to be clear again, I do not disregard your proposal in itself, but it is not as general as the general subscription, with more or less the same code basis behind. Two asides: Of course, the global version should remain sublocale l e. It should not be turned into sublocale (in l) e foo (in l) … is equivalent to context l begin foo … end by construction. We cannot have just one of them. This change was motivated by the realisation that interpretation between locales essentially means changing the module hierarchy. This is a remarkable feature for a module system, which deserves emphasis and isn't really appropriately described by 'interpretation' It is also notable that we have definitions in locales (although this is far beneath your great achievements with sublocale etc.). With them it is the case that we provide them *uniformly* for theories, locales and other targets (something which has been commented as seemingly trivial, »but maybe this is the achievement.« ). Cheers, Florian -- 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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de: Let those thoughts sink further few days. If there is no veto until Apr 7th, I would go ahead to turn the patches upstream. You have proposed a change about which doubts were raised. I don't consider it acceptable to then announce a deadline after which you will go ahead and push. People simply may not be able to respond in time, especially in a vacation period. Regarding interpretation vs sublocale We are talking about user interface design, and this means choosing appropriate metaphors for what certain commands do. People familiar with the history of locales may remember that the precursor of the sublocale command was interpretation l e before I changed that to sublocale in the reimplementation. This change was motivated by the realisation that interpretation between locales essentially means changing the module hierarchy. This is a remarkable feature for a module system, which deserves emphasis and isn't really appropriately described by 'interpretation'. In contrast, interpretation in theories just interprets locales in theories (even though with subscription), there is no additional value. From this perspective (which is the perspective of the designer!) it seems wrong to put interpretation in locales and theories in one category, and local interpretation (as it might be called) in locale contexts and in proof contexts in the other. Even, if this made some aspects of the implementation more elegant. Let me note that, of course, the user interface design should not make the implementation unnecessarily complicated (but I believe we are far away from that). In this light, if a version of the sublocale command seems necessary in context blocks, why no call it 'sublocale'? Of course, the global version should remain sublocale l e. It should not be turned into sublocale (in l) e because the former much more clearly indicates the change to the locale hierarchy. This design has the additional benefits that users don't need to change existing proof documents, terminology in the literature remains up to date, and, most importantly, the sublocale command is clearly recognisable in context blocks. There were two more aspects in the recent discussion. I will pick them up in separate e-mails since this has got too long already. Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de: Let those thoughts sink further few days. If there is no veto until Apr 7th, I would go ahead to turn the patches upstream. Well, here is my veto. I don't see that much of a discussion has taken place yet, and I am very unhappy about the concepts and terminology you are trying to introduce. As you are aware, I do have another job, which makes responding as quickly as you would like impossible. I do hope, though, that we can get this discussion further within this month. Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
On Wed, 27 Mar 2013, Florian Haftmann wrote: After one further round of thinking, I would still suggest * »interpretation« for interpretation without subscription * »subscription« for interpretation with subscription I think it is worth to distinguish these on the surface. Maybe future will bring different possibilities with »private« or whatever. But interpretation is still rare enough that one further change of surface syntax is not that tremendous to end users. Right now we should merely have clear terminology in the discussion. The language keywords can be finalized later. Note that 'interpret' within a local proof context is also without subscription -- as a consequence of how that works. I also agree with you now that 'private' should be just about superficial name space issues (potentially with notation, i.e. things of the syntax_declaration category). So it can stay outside of the considerations here. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
Right now we should merely have clear terminology in the discussion. The language keywords can be finalized later. Indeed. In this delicate corner, modifying surface syntax makes little headache. Lets get right the mental model and the internal implementation first. Note that 'interpret' within a local proof context is also without subscription -- as a consequence of how that works. This is one of the reasons why I think having »interpretation« for non-subscripting interpretations is a good idea. I also agree with you now that 'private' should be just about superficial name space issues (potentially with notation, i.e. things of the syntax_declaration category). So it can stay outside of the considerations here. OK. This simplifies the picture again. So, after these discussions, I would aim for the following: * Using the existing patches as base, provide »subscription«. Keep »sublocale« and »interpretation« as legacy. * Amend the still existing flaws (reinit, subscription in instantiation, …). * Aim for providing non-subscripting interpretation via »interpretation«. »interpretation« on the theory level (which is not possible due to the architecture for the local theories stack) would then issue a legacy warning and resolve to »subscription«, until this behaviour and »sublocale« are discontinued in a further iteration. Let those thoughts sink further few days. If there is no veto until Apr 7th, I would go ahead to turn the patches upstream. Thank you a lot, Florian -- 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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
On Tue, 26 Mar 2013, Makarius wrote: Semantically, do you remember reasons why we did not consider it so far, or was it just forgotton or lost in state-budget problems? I now recall some aspects from the wild days of all that (2006/2007), when we built up that national debt. (Unlike Cyprus we managed to reduce it over the years.) At some point I was always speaking about interpretation (in ...), Florian made his 'subclass' command, and Clemens his 'sublocale'. It was all moving forwards, but without full convergence. So maybe we have a chance now several years later. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
On Wed, 27 Mar 2013, Makarius wrote: Note that we have one more aspect in the back-end that could help here: the 'private' modifier. The back-end above should be read as back-hand, although these are homophones for Frenchmen. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
context B begin interpretation A interpretation A' interpretation A'' end sublocale B A'' What you currently have in many places (e.g. http://isabelle.in.tum.de/reports/Isabelle/file/757fa47af981/src/HOL/Lattices.thy) is the pattern. context B begin … end sublocale B … context B begin … end sublocale B … context B begin … end When giving up the paradigm that sublocale dependencies may only be introduced on the global level, youo end up with sth like context B begin … intepretation … … intepretation … … end which is compacter and more intuitive. Florian -- 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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
You might still argue about syntax, e.g. having separate commands subscription – what is currently interpretation and subscription, not in free-floating contexts (as implemented in the patches). interpretation – only in confined contexts (locales, context begin … end, but not global theories any longer) without any subscription. That paragraph is very difficult to understand. OK, another attempt. You can also have two distinguished commands * subscription – interpretation with permanent subscription * interpretation – without any subscriptions By their very nature, interpretation would not be possible on the global level, and subscription would not be possible in unnamed contexts. Note that we have one more aspect in the back-end that could help here: the 'private' modifier. Its meaning was not fully defined so far, but it could do the job: context B begin private interpretation A ... private interpretation A' ... private interpretation A'' ... interpretation A'' ... end Until I manage to get 'private' as command modifier into the toplevel interpreter, we can tentatively use 'private_interpretation'. So the proposal would be to have two commands * interpretation (»subscription« from above) * private_interpretation (»interpretation« from above) Until now I have been thinking about »private« to be a certain name space policy. I don't forsee how exactly this relates to subscriptions. Maybe it is a different thing. For this reason I would prefer my own naming scheme at the moment. Cheers, Florian -- 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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
After one further round of thinking, I would still suggest * »interpretation« for interpretation without subscription * »subscription« for interpretation with subscription I think it is worth to distinguish these on the surface. Maybe future will bring different possibilities with »private« or whatever. But interpretation is still rare enough that one further change of surface syntax is not that tremendous to end users. Florian -- 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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
On Sun, 24 Mar 2013, Florian Haftmann wrote: There is a series of minimal invasive patches to generalize »interpretation« / »sublocale« to »interpretation« in arbitrary targets, not just theories and locales. The patches are inspectible at http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation OK, lets see if we get some actual work done here ... In the first round of just eye-balling this looks formally correct to me. (I will look more closely a bit later.) Semantically, do you remember reasons why we did not consider it so far, or was it just forgotton or lost in state-budget problems? We have a little bit of budget now after the release and towards the summer, but we need to stay within a reasonable range of complexity. Clemens Ballaring might also have an informed opinion on that -- I've just seen some locale-related activitity by him (e.g. c3eb0b517ced). * Amend the instantiation target not to choke on abbreviations stemming from interpretations. Most problems of computer-science can be reduced to abbreviations within local contexts in Isabelle :-) Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
Semantically, do you remember reasons why we did not consider it so far, or was it just forgotton or lost in state-budget problems? We have a little bit of budget now after the release and towards the summer, but we need to stay within a reasonable range of complexity. Well, we always have considered it as a possibility. For the moment I think it is a reasonable thing because it is almost suggested by the code itself »as it is« . Clemens Ballaring might also have an informed opinion on that -- I've just seen some locale-related activitity by him (e.g. c3eb0b517ced). I'm looking forward to that. Florian -- 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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
Hi Florian, I'm in favour of generalising interpretation to targets, but in my opinion it would not be right to provide the sublocale command as the interpretation command in a locale context. There are two reasons: 1. sublocale modifies the locale graph of the underlying theory. This is a big change and shouldn't happen as a side effect of a command in a target context. 2. sublocale and interpretation are more different than it looks: interpretation provides inheritance of mixins (or, from the user perspective, rewrite morphisms) and it is possible to amend mixins in interpretation (currently only through the API). On the other hand, I see that interpretation in a locale context can help working in an incremental fashion in such a context (which I assume is the motivation for your patches). So, what should interpretation in a locale be like? Currently, sublocale is used for two purposes: a) relating two locales to each other (such as a total order is a lattice) b) import (a typically small number of) lemmas, which are needed for establishing some result, from one locale A into another locale B While sublocale is perfect for a), in b) there is a big overhead caused by importing all theorems from A into B whenever B is activated, while all that's needed is importing theorems from A to B once. The latter is what we should try to address by a variant of the interpretation command for locale contexts. Here's my proposal: context B begin ... interpretation A ... end makes the interpretation of A available in the block up to the closing 'end'. The interpretation will not be persisted; results are only available temporarily to aid establishing some results in B. Of course, this would mean that the literal command interpretation (in B) A is useless, but that wouldn't hurt. On the other hand, if users started to use this feature, locale hierarchies could become less complex and, as a consequence, theories faster (well, become slower more slowly...). When interpreting a hierarchy A - A' - A'' incrementally, the pattern would be context B begin interpretation A interpretation A' interpretation A'' end sublocale B A'' that is, one additional sublocale declaration would be sufficient to persist the incremental development. What do you think of these ideas? I would appreciate, if you could work towards them (I myself never quite mastered the intricacies of the ML level target code). Clemens Quoting Florian Haftmann florian.haftm...@informatik.tu-muenchen.de: There is a series of minimal invasive patches to generalize »interpretation« / »sublocale« to »interpretation« in arbitrary targets, not just theories and locales. The patches are inspectible at http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation Explanations follow. It is good tradition not to muddle with the module system code arbitrarily, therefore this rather unconventional approach to gain feedback. 1. http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/21821401c5a5 Identity juggling to prepare following steps. 2. http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/aee4c6577ff7 Ironing out a FIXME in the code. This already gives a hint how the existing code base naturally converges to unify »interpretation« and »sublocale«. 3. http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/f6bc704b5cd6 In order to let »interpretation« and »sublocale« converge, the close marriage of »interpretation« and »interpret« must be given up. This is a step back only in the first instance ? it would still be possible to factor out common code of the resulting unified »interpretation« and »interpret« in a separate step afterwards. In the same breath the (operationally void!) switch from »ctxt« to »lthy« yields the key clue of the whole story. 4. http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/9d5c8a5251d5 This establishes sharing of »interpretation« and »sublocale« as far as appropriate. 5. http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/1d3a62ef74dd Identity juggling to prepare following steps. 6. http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/dd6dd81381fb This is the key step: »subscription« as target operation to make »interpretation« work regardless of the underlying target. The »potential_reinit« is a wart: when interpreting locales into locales, the new facts must be provided in the local theory context of this locale also, and I have up after a few experiments with Locale.activate_facts etc. Note the same situation has been occuring in »subclass« for years now. Here it is more critical since interpretation should be fully target-ignorant (unlike subclass which always knows that it operates on classes). However I have let it stand for the moment as a conceptual preview. I'm
Re: [isabelle-dev] Interpretation in arbitrary targets.
Hi Clemens,
nice to hear from you.
Let me add my perspective here, and see how we can converge.
2. sublocale and interpretation are more different than it looks:
interpretation provides inheritance of mixins (or, from the user
perspective, rewrite morphisms) and it is possible to amend mixins in
interpretation (currently only through the API).
Yes. The underlying primitive mechanisms (I tend to follow locale.ML
here and call them »registrations« and »dependencies«) are different and
will always be.
On the other hand, I see that interpretation in a locale context can
help working in an incremental fashion in such a context (which I assume
is the motivation for your patches).
So, what should interpretation in a locale be like? Currently,
sublocale is used for two purposes:
a) relating two locales to each other (such as a total order is a
lattice)
b) import (a typically small number of) lemmas, which are needed for
establishing some result, from one locale A into another locale B
Ack. I tend to compare a) with a watering can. There is currently no
chance to achieve b) except inside proofs. b) would be one of the most
important use cases for locales also, since the watering can is only
appropriate in very »canonical« situations, type classes being one
prominent case. In my terminology, I tend to call a) »subscription«, to
emphasize the permanent character.
But note that in my way of thinking, the current »interpretation« and
»sublocale« commands are different facets of »subscription«. Indeed, I
was first considering to rename the target-sensitive interpretation
command »subscription«. However the name does not so much matter for
me. Now your argument is that »interpretation« and »sublocale« should
be kept apart since they are implemented by different means
(»registrations« vs. »dependencies). But this is what local theories
are about: abstract over the common essence. That the underlying
primitive mechanisms also allow different things should not bother here:
e.g. you can add axioms to global theories but not to locales, but this
does not invalidate the local theory concept either.
1. sublocale modifies the locale graph of the underlying theory. This
is a big change and shouldn't happen as a side effect of a command in a
target context.
Changing the underlying target is the essence of commands in target
contexts – in the case of interpretation (in …), it is not a side
effect, but the central issue. You might argue that »interpretation«
suggests a different thing, but maybe then we have to choose a different
name for that, see above.
But see now how scenario b) would integrate into my design. Recently
the local theory concept has been enriched with free-floating contexts
context
fixes … assumes …
begin
…
end
Now what would
context
…
begin
…
interpretation
…
end
be? Currently, there is check that »interpretation« may only be issued
at the bottom level of the local theory stack, outside any free-floating
context. Although I have no constructive proof at hand yet, I believe
that by lifting the check appropriately we get b) for free: similar to
»interpret«, this would only yield facts inside the context (whose
bindings disappear after »end«) without any additional dependencies or
registrations. This is also why I adhered to »interpretation« in the
end. So, your example could somehow look like
context B begin
context
begin
interpretation A
end
context
begin
interpretation A'
end
context
begin
interpretation A''
end
interpretation A'' -- {* permanent subscription *}
end
You might still argue about syntax, e.g. having separate commands
subscription – what is currently interpretation and subscription, not
in free-floating contexts (as implemented in the patches).
interpretation – only in confined contexts (locales, context begin …
end, but not global theories any longer) without any subscription.
Overall I am amazed how well this all would fit to the existing local
theories.
What do you think of these ideas? I would appreciate, if you could work
towards them (I myself never quite mastered the intricacies of the ML
level target code).
Restarting after some years left aside, I slowly start to comprehend the
details…
Cheers,
Florian
--
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
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Interpretation in arbitrary targets.
On Tue, 26 Mar 2013, Florian Haftmann wrote: Recently the local theory concept has been enriched with free-floating contexts context fixes … assumes … begin … end Now what would context … begin … interpretation … end be? Currently, there is check that »interpretation« may only be issued at the bottom level of the local theory stack, outside any free-floating context. Although I have no constructive proof at hand yet, I believe that by lifting the check appropriately we get b) for free: similar to »interpret«, this would only yield facts inside the context (whose bindings disappear after »end«) without any additional dependencies or registrations. (I still need to study the material on this thread carefully. Right now just a quick interjection.) Does that mean that 'interpretation' within unnamed 'context begin ... end' is without permanent subscription, but in a named target context or the global theory it is still with subscription as before? Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Interpretation in arbitrary targets.
There is a series of minimal invasive patches to generalize »interpretation« / »sublocale« to »interpretation« in arbitrary targets, not just theories and locales. The patches are inspectible at http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation Explanations follow. It is good tradition not to muddle with the module system code arbitrarily, therefore this rather unconventional approach to gain feedback. 1. http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/21821401c5a5 Identity juggling to prepare following steps. 2. http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/aee4c6577ff7 Ironing out a FIXME in the code. This already gives a hint how the existing code base naturally converges to unify »interpretation« and »sublocale«. 3. http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/f6bc704b5cd6 In order to let »interpretation« and »sublocale« converge, the close marriage of »interpretation« and »interpret« must be given up. This is a step back only in the first instance – it would still be possible to factor out common code of the resulting unified »interpretation« and »interpret« in a separate step afterwards. In the same breath the (operationally void!) switch from »ctxt« to »lthy« yields the key clue of the whole story. 4. http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/9d5c8a5251d5 This establishes sharing of »interpretation« and »sublocale« as far as appropriate. 5. http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/1d3a62ef74dd Identity juggling to prepare following steps. 6. http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/dd6dd81381fb This is the key step: »subscription« as target operation to make »interpretation« work regardless of the underlying target. The »potential_reinit« is a wart: when interpreting locales into locales, the new facts must be provided in the local theory context of this locale also, and I have up after a few experiments with Locale.activate_facts etc. Note the same situation has been occuring in »subclass« for years now. Here it is more critical since interpretation should be fully target-ignorant (unlike subclass which always knows that it operates on classes). However I have let it stand for the moment as a conceptual preview. I'm thankful for any hints how to resolve this. In this change the clone in src/Tools/ has been changed accordingly – its future is still not so clear yet. 7. http://isabelle.in.tum.de/~haftmann/cgi-bin/repos/interpretation/rev/f48553718a7a Some examples. Note that I have experienced that »interpretation« does sometimes not work inside »instantiation« (something in connection with abbreviations), but this indicates a weakness of the instantiation target rather than a conceptual mistake in interpretation. This needs to be amended separately. The next steps after those would be something like * Amend the wart mentioned in (6). * Add documentation. * One round trip over the whole sources to avoid references to (then legacy) »sublocale«. * Amend the instantiation target not to choke on abbreviations stemming from interpretations. * Examine whether this code basis already allows to have confined interpretations inside context … begin … end blocks. I'm looking forward to responses. Cheers, Florian -- 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 isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
