Re: [isabelle-dev] Interpretation in arbitrary targets.

2013-04-17 Thread Clemens Ballarin
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

Re: [isabelle-dev] Interpretation in arbitrary targets.

2013-04-17 Thread 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