--- a/NEWS Wed Dec 09 21:20:56 2015 +0100
+++ b/NEWS Mon Dec 07 10:49:08 2015 +0100
@@ -346,12 +346,12 @@
notation right.derived ("\<odot>''")
end
-* Command 'sublocale' accepts mixin definitions after keyword
+* Command 'sublocale' accepts rewrite definitions after keyword
'defines'.
* Command 'permanent_interpretation' is available in Pure, without
need to load a separate theory. Keyword 'defines' identifies
-mixin definitions, keyword 'rewrites' identifies rewrite morphisms.
+rewrite definitions, keyword 'rewrites' identifies rewrite equations.
INCOMPATIBILITY.
* Command 'print_definitions' prints dependencies of definitional
--- a/src/Doc/Isar_Ref/Spec.thy Wed Dec 09 21:20:56 2015 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Mon Dec 07 10:49:08 2015 +0100
@@ -670,7 +670,9 @@
proved explicitly the user. Such rewrite definitions are a even more useful
device for interpreting concepts introduced through definitions, but they
are only supported for interpretation commands operating in a local theory
- whose implementing target actually supports this.
+ whose implementing target actually supports this. Note that despite
+ the suggestive \<^theory_text>\<open>and\<close> connective, \<open>defs\<close>
+ are parsed sequentially without mutual recursion.
\<^descr> \<^theory_text>\<open>interpretation expr rewrites eqns\<close> interprets \<open>expr\<close> into a local theory
such that its lifetime is limited to the current context block (e.g. a
@@ -773,6 +775,13 @@
\end{warn}
\begin{warn}
+ Due to a technical limitation, the specific context of a interpretation
+ given by a \<^theory_text>\<open>for\<close> clause can get lost between a \<^theory_text>\<open>defines\<close> and
+ \<^theory_text>\<open>rewrites\<close> clause and must then be recovered manually using
+ explicit sort constraints and quantified term variables.
+ \end{warn}
+
+ \begin{warn}
While \<^theory_text>\<open>interpretation (in c) \<dots>\<close> is admissible, it is not useful since
its result is discarded immediately.
\end{warn}
--- a/src/Pure/Isar/interpretation.ML Wed Dec 09 21:20:56 2015 +0100
+++ b/src/Pure/Isar/interpretation.ML Mon Dec 07 10:49:08 2015 +0100
@@ -177,7 +177,7 @@
end;
-(* algebraic-view *)
+(* algebraic view *)
local