clarified terminology
authorhaftmann
Mon Dec 07 10:49:08 2015 +0100 (2015-12-07)
changeset 618235daa82ba4078
parent 61822 a16497c686cb
child 61824 dcbe9f756ae0
clarified terminology
NEWS
src/Doc/Isar_Ref/Spec.thy
src/Pure/Isar/interpretation.ML
     1.1 --- a/NEWS	Wed Dec 09 21:20:56 2015 +0100
     1.2 +++ b/NEWS	Mon Dec 07 10:49:08 2015 +0100
     1.3 @@ -346,12 +346,12 @@
     1.4      notation right.derived ("\<odot>''")
     1.5    end
     1.6  
     1.7 -* Command 'sublocale' accepts mixin definitions after keyword
     1.8 +* Command 'sublocale' accepts rewrite definitions after keyword
     1.9  'defines'.
    1.10  
    1.11  * Command 'permanent_interpretation' is available in Pure, without
    1.12  need to load a separate theory.  Keyword 'defines' identifies
    1.13 -mixin definitions, keyword 'rewrites' identifies rewrite morphisms.
    1.14 +rewrite definitions, keyword 'rewrites' identifies rewrite equations.
    1.15  INCOMPATIBILITY.
    1.16  
    1.17  * Command 'print_definitions' prints dependencies of definitional
     2.1 --- a/src/Doc/Isar_Ref/Spec.thy	Wed Dec 09 21:20:56 2015 +0100
     2.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Mon Dec 07 10:49:08 2015 +0100
     2.3 @@ -670,7 +670,9 @@
     2.4    proved explicitly the user. Such rewrite definitions are a even more useful
     2.5    device for interpreting concepts introduced through definitions, but they
     2.6    are only supported for interpretation commands operating in a local theory
     2.7 -  whose implementing target actually supports this.
     2.8 +  whose implementing target actually supports this.  Note that despite
     2.9 +  the suggestive \<^theory_text>\<open>and\<close> connective, \<open>defs\<close>
    2.10 +  are parsed sequentially without mutual recursion.
    2.11  
    2.12    \<^descr> \<^theory_text>\<open>interpretation expr rewrites eqns\<close> interprets \<open>expr\<close> into a local theory
    2.13    such that its lifetime is limited to the current context block (e.g. a
    2.14 @@ -773,6 +775,13 @@
    2.15    \end{warn}
    2.16  
    2.17    \begin{warn}
    2.18 +    Due to a technical limitation, the specific context of a interpretation
    2.19 +    given by a \<^theory_text>\<open>for\<close> clause can get lost between a \<^theory_text>\<open>defines\<close> and
    2.20 +    \<^theory_text>\<open>rewrites\<close> clause and must then be recovered manually using
    2.21 +    explicit sort constraints and quantified term variables.
    2.22 +  \end{warn}
    2.23 +
    2.24 +  \begin{warn}
    2.25      While \<^theory_text>\<open>interpretation (in c) \<dots>\<close> is admissible, it is not useful since
    2.26      its result is discarded immediately.
    2.27    \end{warn}
     3.1 --- a/src/Pure/Isar/interpretation.ML	Wed Dec 09 21:20:56 2015 +0100
     3.2 +++ b/src/Pure/Isar/interpretation.ML	Mon Dec 07 10:49:08 2015 +0100
     3.3 @@ -177,7 +177,7 @@
     3.4  end;
     3.5  
     3.6  
     3.7 -(* algebraic-view *)
     3.8 +(* algebraic view *)
     3.9  
    3.10  local
    3.11