src/Pure/Isar/interpretation.ML
14 months ago wenzelm 2018-08-30 tuned;
14 months ago wenzelm 2018-08-30 tuned;
20 months ago ballarin 2018-03-06 Drop rewrite rule arguments of sublocale and interpretation implementations.
20 months ago ballarin 2018-03-02 Proper rewrite morphisms in locale instances.
20 months ago wenzelm 2018-02-23 command 'interpret' no longer exposes resulting theorems as literal facts;
22 months ago ballarin 2018-01-16 Experimental support for rewrite morphisms in locale instances.
2017-08-04 haftmann 2017-08-04 provide explicit variant initializers for regular named target vs. almost-named target
2016-07-06 wenzelm 2016-07-06 tuned signature;
2016-07-04 wenzelm 2016-07-04 clarified positions, e.g. for reports on literal facts;
2016-07-04 wenzelm 2016-07-04 tuned whitespace;
2016-07-04 wenzelm 2016-07-04 tuned;
2016-07-04 wenzelm 2016-07-04 tuned;
2016-06-23 wenzelm 2016-06-23 tuned signature;
2016-04-28 wenzelm 2016-04-28 unfold is subject to unfold_abs_def (still inactive); tuned signature;
2016-03-21 wenzelm 2016-03-21 eliminated unused argument (see also 58110c1e02bc);
2015-12-19 haftmann 2015-12-19 abandoned attempt to unify sublocale and interpretation into global theories
2015-12-07 haftmann 2015-12-07 clarified terminology
2015-12-02 haftmann 2015-12-02 alternating parsing and defining of rewrite definitions: formally correct treatment of polymorphism
2015-12-02 haftmann 2015-12-02 prefer conventional read/check distinction over manual check
2015-12-02 haftmann 2015-12-02 clarified role of context for reading rewrite specifications
2015-12-02 haftmann 2015-12-02 formally correct context for export, which got screwed up in 87203a0f0041
2015-12-02 haftmann 2015-12-02 tuned whitespace
2015-11-19 haftmann 2015-11-19 explicit nested local theory for definitions, however retaining arcane low-level fiddling with background theory
2015-11-18 wenzelm 2015-11-18 make SML/NJ happy;
2015-11-16 haftmann 2015-11-16 clarified contexts by factoring out reading and definition of mixins
2015-11-15 haftmann 2015-11-15 formally correct context for export
2015-11-15 haftmann 2015-11-15 tuned whitespace
2015-11-14 haftmann 2015-11-14 represent both algebraic and local-theory views on locale interpretation in interfaces
2015-11-14 haftmann 2015-11-14 tuned -- share implementations as far as appropriate
2015-11-14 haftmann 2015-11-14 coalesce permanent_interpretation.ML with interpretation.ML
2015-11-14 haftmann 2015-11-14 separate ML module for interpretation