eliminated \<Colon> from syntax of constraints;
authorwenzelm
Wed Sep 09 14:47:41 2015 +0200 (2015-09-09)
changeset 611435f898411ce87
parent 61142 6d29eb7c5fb2
child 61144 5e94dfead1c2
eliminated \<Colon> from syntax of constraints;
NEWS
src/Doc/Codegen/Setup.thy
src/Doc/Isar_Ref/Inner_Syntax.thy
src/HOL/Imperative_HOL/Overview.thy
src/HOL/Library/OptionalSugar.thy
src/HOL/SPARK/Manual/Reference.thy
src/Pure/pure_thy.ML
     1.1 --- a/NEWS	Wed Sep 09 11:24:34 2015 +0200
     1.2 +++ b/NEWS	Wed Sep 09 14:47:41 2015 +0200
     1.3 @@ -209,6 +209,10 @@
     1.4    type_notation Map.map  (infixr "~=>" 0)
     1.5    notation Map.map_comp  (infixl "o'_m" 55)
     1.6  
     1.7 +* The alternative notation "\<Colon>" for type and sort constraints has been
     1.8 +removed: in LaTeX document output it looks the same as "::".
     1.9 +INCOMPATIBILITY, use plain "::" instead.
    1.10 +
    1.11  * Case combinator "prod_case" with eta-contracted body functions
    1.12  has explicit "uncurry" notation, to provide a compact notation while
    1.13  getting ride of a special case translation.  Slight syntactic
     2.1 --- a/src/Doc/Codegen/Setup.thy	Wed Sep 09 11:24:34 2015 +0200
     2.2 +++ b/src/Doc/Codegen/Setup.thy	Wed Sep 09 14:47:41 2015 +0200
     2.3 @@ -11,18 +11,13 @@
     2.4  ML_file "../antiquote_setup.ML"
     2.5  ML_file "../more_antiquote.ML"
     2.6  
     2.7 -setup \<open>
     2.8 -let
     2.9 -  val typ = Simple_Syntax.read_typ;
    2.10 -in
    2.11 -  Sign.del_syntax (Symbol.xsymbolsN, false)
    2.12 -   [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
    2.13 -    ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
    2.14 -  Sign.add_syntax (Symbol.xsymbolsN, false)
    2.15 -   [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
    2.16 -    ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
    2.17 -end
    2.18 -\<close>
    2.19 +no_syntax (output)
    2.20 +  "_constrain" :: "logic => type => logic"  ("_::_" [4, 0] 3)
    2.21 +  "_constrain" :: "prop' => type => prop'"  ("_::_" [4, 0] 3)
    2.22 +
    2.23 +syntax (output)
    2.24 +  "_constrain" :: "logic => type => logic"  ("_ :: _" [4, 0] 3)
    2.25 +  "_constrain" :: "prop' => type => prop'"  ("_ :: _" [4, 0] 3)
    2.26  
    2.27  declare [[default_code_width = 74]]
    2.28  
     3.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Sep 09 11:24:34 2015 +0200
     3.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Wed Sep 09 14:47:41 2015 +0200
     3.3 @@ -839,10 +839,6 @@
     3.4    input is likely to be ambiguous.  The correct form is @{text "x < (y
     3.5    :: nat)"}.
     3.6  
     3.7 -  \item Constraints may be either written with two literal colons
     3.8 -  ``@{verbatim "::"}'' or the double-colon symbol @{verbatim "\<Colon>"},
     3.9 -  which actually looks exactly the same in some {\LaTeX} styles.
    3.10 -
    3.11    \item Dummy variables (written as underscore) may occur in different
    3.12    roles.
    3.13  
     4.1 --- a/src/HOL/Imperative_HOL/Overview.thy	Wed Sep 09 11:24:34 2015 +0200
     4.2 +++ b/src/HOL/Imperative_HOL/Overview.thy	Wed Sep 09 14:47:41 2015 +0200
     4.3 @@ -8,18 +8,14 @@
     4.4  begin
     4.5  
     4.6  (* type constraints with spacing *)
     4.7 -setup {*
     4.8 -let
     4.9 -  val typ = Simple_Syntax.read_typ;
    4.10 -in
    4.11 -  Sign.del_syntax (Symbol.xsymbolsN, false)
    4.12 -   [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
    4.13 -    ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
    4.14 -  Sign.add_syntax (Symbol.xsymbolsN, false)
    4.15 -   [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon>  _", [4, 0], 3)),
    4.16 -    ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
    4.17 -end
    4.18 -*}(*>*)
    4.19 +no_syntax (output)
    4.20 +  "_constrain" :: "logic => type => logic"  ("_::_" [4, 0] 3)
    4.21 +  "_constrain" :: "prop' => type => prop'"  ("_::_" [4, 0] 3)
    4.22 +
    4.23 +syntax (output)
    4.24 +  "_constrain" :: "logic => type => logic"  ("_ :: _" [4, 0] 3)
    4.25 +  "_constrain" :: "prop' => type => prop'"  ("_ :: _" [4, 0] 3)
    4.26 +(*>*)
    4.27  
    4.28  text {*
    4.29    @{text "Imperative HOL"} is a leightweight framework for reasoning
     5.1 --- a/src/HOL/Library/OptionalSugar.thy	Wed Sep 09 11:24:34 2015 +0200
     5.2 +++ b/src/HOL/Library/OptionalSugar.thy	Wed Sep 09 14:47:41 2015 +0200
     5.3 @@ -48,14 +48,13 @@
     5.4    "_bind (CONST DUMMY # p) e" <= "_bind p (CONST tl e)"
     5.5  
     5.6  (* type constraints with spacing *)
     5.7 +no_syntax (output)
     5.8 +  "_constrain" :: "logic => type => logic"  ("_::_" [4, 0] 3)
     5.9 +  "_constrain" :: "prop' => type => prop'"  ("_::_" [4, 0] 3)
    5.10  
    5.11 -no_syntax (xsymbols output)
    5.12 -  "_constrain" :: "logic => type => logic"  ("_\<Colon>_" [4, 0] 3)
    5.13 -  "_constrain" :: "prop' => type => prop'"  ("_\<Colon>_" [4, 0] 3)
    5.14 -
    5.15 -syntax (xsymbols output)
    5.16 -  "_constrain" :: "logic => type => logic"  ("_ \<Colon> _" [4, 0] 3)
    5.17 -  "_constrain" :: "prop' => type => prop'"  ("_ \<Colon> _" [4, 0] 3)
    5.18 +syntax (output)
    5.19 +  "_constrain" :: "logic => type => logic"  ("_ :: _" [4, 0] 3)
    5.20 +  "_constrain" :: "prop' => type => prop'"  ("_ :: _" [4, 0] 3)
    5.21  
    5.22  
    5.23  (* sorts as intersections *)
     6.1 --- a/src/HOL/SPARK/Manual/Reference.thy	Wed Sep 09 11:24:34 2015 +0200
     6.2 +++ b/src/HOL/SPARK/Manual/Reference.thy	Wed Sep 09 14:47:41 2015 +0200
     6.3 @@ -4,7 +4,7 @@
     6.4  begin
     6.5  
     6.6  syntax (my_constrain output)
     6.7 -  "_constrain" :: "logic => type => logic" ("_ \<Colon> _" [4, 0] 3)
     6.8 +  "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3)
     6.9  (*>*)
    6.10  
    6.11  chapter {* HOL-\SPARK{} Reference *}
     7.1 --- a/src/Pure/pure_thy.ML	Wed Sep 09 11:24:34 2015 +0200
     7.2 +++ b/src/Pure/pure_thy.ML	Wed Sep 09 14:47:41 2015 +0200
     7.3 @@ -176,11 +176,6 @@
     7.4    #> Sign.add_syntax (Symbol.xsymbolsN, true)
     7.5     [(tycon "fun",         typ "type => type => type",   Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
     7.6      ("_bracket",          typ "types => type => type",  Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
     7.7 -    ("_ofsort",           typ "tid_position => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
     7.8 -    ("_constrain",        typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
     7.9 -    ("_constrain",        typ "prop' => type => prop'", Mixfix ("_\\<Colon>_", [4, 0], 3)),
    7.10 -    ("_idtyp",            typ "id_position => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
    7.11 -    ("_idtypdummy",       typ "type => idt",            Mixfix ("'_()\\<Colon>_", [], 0)),
    7.12      ("_lambda",           typ "pttrns => 'a => logic",  Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
    7.13      (const "Pure.eq",     typ "'a => 'a => prop",       Infix ("\\<equiv>", 2)),
    7.14      (const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),