discontinued \<struct> syntax;
authorwenzelm
Sat Jan 09 12:35:07 2016 +0100 (2016-01-09)
changeset 62107f74a33b14200
parent 62106 d6af554512d7
child 62108 0046bacc5f5b
discontinued \<struct> syntax;
NEWS
src/Doc/Isar_Ref/Inner_Syntax.thy
src/Pure/pure_thy.ML
     1.1 --- a/NEWS	Fri Jan 08 20:06:48 2016 +0100
     1.2 +++ b/NEWS	Sat Jan 09 12:35:07 2016 +0100
     1.3 @@ -342,6 +342,10 @@
     1.4  * Keyword 'rewrites' identifies rewrite morphisms in interpretation
     1.5  commands. Previously, the keyword was 'where'. INCOMPATIBILITY.
     1.6  
     1.7 +* Special notation \<struct> for the first implicit 'structure' in the context
     1.8 +has been discontinued. Rare INCOMPATIBILITY, use explicit structure name
     1.9 +instead, notably in indexed notation with block-subscript (e.g. \<odot>\<^bsub>A\<^esub>).
    1.10 +
    1.11  * More gentle suppression of syntax along locale morphisms while
    1.12  printing terms. Previously 'abbreviation' and 'notation' declarations
    1.13  would be suppressed for morphisms except term identity. Now
     2.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Fri Jan 08 20:06:48 2016 +0100
     2.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Jan 09 12:35:07 2016 +0100
     2.3 @@ -656,7 +656,6 @@
     2.4      & \<open>|\<close> & \<^verbatim>\<open>CONST\<close> \<open>id  |\<close>~~\<^verbatim>\<open>CONST\<close> \<open>longid\<close> \\
     2.5      & \<open>|\<close> & \<^verbatim>\<open>XCONST\<close> \<open>id  |\<close>~~\<^verbatim>\<open>XCONST\<close> \<open>longid\<close> \\
     2.6      & \<open>|\<close> & \<open>logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)  any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> & \<open>(999)\<close> \\
     2.7 -    & \<open>|\<close> & \<open>\<struct> index\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> \\
     2.8      & \<open>|\<close> & \<^verbatim>\<open>%\<close> \<open>pttrns\<close> \<^verbatim>\<open>.\<close> \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\
     2.9      & \<open>|\<close> & \<open>\<lambda>\<close> \<open>pttrns\<close> \<^verbatim>\<open>.\<close> \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\
    2.10      & \<open>|\<close> & \<^verbatim>\<open>op\<close> \<^verbatim>\<open>==\<close>~~\<open>|\<close>~~\<^verbatim>\<open>op\<close> \<open>\<equiv>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>op\<close> \<^verbatim>\<open>&&&\<close> \\
     3.1 --- a/src/Pure/pure_thy.ML	Fri Jan 08 20:06:48 2016 +0100
     3.2 +++ b/src/Pure/pure_thy.ML	Sat Jan 09 12:35:07 2016 +0100
     3.3 @@ -151,7 +151,7 @@
     3.4      ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
     3.5      ("_indexdefault", typ "index",                     Delimfix ""),
     3.6      ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
     3.7 -    ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
     3.8 +    ("_struct",     typ "index => logic",              NoSyn),
     3.9      ("_update_name", typ "idt",                        NoSyn),
    3.10      ("_constrainAbs", typ "'a",                        NoSyn),
    3.11      ("_position_sort", typ "tid => tid_position",      Delimfix "_"),