--- a/NEWS Wed Sep 09 11:24:34 2015 +0200
+++ b/NEWS Wed Sep 09 14:47:41 2015 +0200
@@ -209,6 +209,10 @@
type_notation Map.map (infixr "~=>" 0)
notation Map.map_comp (infixl "o'_m" 55)
+* The alternative notation "\<Colon>" for type and sort constraints has been
+removed: in LaTeX document output it looks the same as "::".
+INCOMPATIBILITY, use plain "::" instead.
+
* Case combinator "prod_case" with eta-contracted body functions
has explicit "uncurry" notation, to provide a compact notation while
getting ride of a special case translation. Slight syntactic
--- a/src/Doc/Codegen/Setup.thy Wed Sep 09 11:24:34 2015 +0200
+++ b/src/Doc/Codegen/Setup.thy Wed Sep 09 14:47:41 2015 +0200
@@ -11,18 +11,13 @@
ML_file "../antiquote_setup.ML"
ML_file "../more_antiquote.ML"
-setup \<open>
-let
- val typ = Simple_Syntax.read_typ;
-in
- Sign.del_syntax (Symbol.xsymbolsN, false)
- [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
- ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
- Sign.add_syntax (Symbol.xsymbolsN, false)
- [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
- ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
-end
-\<close>
+no_syntax (output)
+ "_constrain" :: "logic => type => logic" ("_::_" [4, 0] 3)
+ "_constrain" :: "prop' => type => prop'" ("_::_" [4, 0] 3)
+
+syntax (output)
+ "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3)
+ "_constrain" :: "prop' => type => prop'" ("_ :: _" [4, 0] 3)
declare [[default_code_width = 74]]
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Wed Sep 09 11:24:34 2015 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Wed Sep 09 14:47:41 2015 +0200
@@ -839,10 +839,6 @@
input is likely to be ambiguous. The correct form is @{text "x < (y
:: nat)"}.
- \item Constraints may be either written with two literal colons
- ``@{verbatim "::"}'' or the double-colon symbol @{verbatim "\<Colon>"},
- which actually looks exactly the same in some {\LaTeX} styles.
-
\item Dummy variables (written as underscore) may occur in different
roles.
--- a/src/HOL/Imperative_HOL/Overview.thy Wed Sep 09 11:24:34 2015 +0200
+++ b/src/HOL/Imperative_HOL/Overview.thy Wed Sep 09 14:47:41 2015 +0200
@@ -8,18 +8,14 @@
begin
(* type constraints with spacing *)
-setup {*
-let
- val typ = Simple_Syntax.read_typ;
-in
- Sign.del_syntax (Symbol.xsymbolsN, false)
- [("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
- ("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
- Sign.add_syntax (Symbol.xsymbolsN, false)
- [("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
- ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
-end
-*}(*>*)
+no_syntax (output)
+ "_constrain" :: "logic => type => logic" ("_::_" [4, 0] 3)
+ "_constrain" :: "prop' => type => prop'" ("_::_" [4, 0] 3)
+
+syntax (output)
+ "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3)
+ "_constrain" :: "prop' => type => prop'" ("_ :: _" [4, 0] 3)
+(*>*)
text {*
@{text "Imperative HOL"} is a leightweight framework for reasoning
--- a/src/HOL/Library/OptionalSugar.thy Wed Sep 09 11:24:34 2015 +0200
+++ b/src/HOL/Library/OptionalSugar.thy Wed Sep 09 14:47:41 2015 +0200
@@ -48,14 +48,13 @@
"_bind (CONST DUMMY # p) e" <= "_bind p (CONST tl e)"
(* type constraints with spacing *)
+no_syntax (output)
+ "_constrain" :: "logic => type => logic" ("_::_" [4, 0] 3)
+ "_constrain" :: "prop' => type => prop'" ("_::_" [4, 0] 3)
-no_syntax (xsymbols output)
- "_constrain" :: "logic => type => logic" ("_\<Colon>_" [4, 0] 3)
- "_constrain" :: "prop' => type => prop'" ("_\<Colon>_" [4, 0] 3)
-
-syntax (xsymbols output)
- "_constrain" :: "logic => type => logic" ("_ \<Colon> _" [4, 0] 3)
- "_constrain" :: "prop' => type => prop'" ("_ \<Colon> _" [4, 0] 3)
+syntax (output)
+ "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3)
+ "_constrain" :: "prop' => type => prop'" ("_ :: _" [4, 0] 3)
(* sorts as intersections *)
--- a/src/HOL/SPARK/Manual/Reference.thy Wed Sep 09 11:24:34 2015 +0200
+++ b/src/HOL/SPARK/Manual/Reference.thy Wed Sep 09 14:47:41 2015 +0200
@@ -4,7 +4,7 @@
begin
syntax (my_constrain output)
- "_constrain" :: "logic => type => logic" ("_ \<Colon> _" [4, 0] 3)
+ "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3)
(*>*)
chapter {* HOL-\SPARK{} Reference *}
--- a/src/Pure/pure_thy.ML Wed Sep 09 11:24:34 2015 +0200
+++ b/src/Pure/pure_thy.ML Wed Sep 09 14:47:41 2015 +0200
@@ -176,11 +176,6 @@
#> Sign.add_syntax (Symbol.xsymbolsN, true)
[(tycon "fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
- ("_ofsort", typ "tid_position => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
- ("_constrain", typ "logic => type => logic", Mixfix ("_\\<Colon>_", [4, 0], 3)),
- ("_constrain", typ "prop' => type => prop'", Mixfix ("_\\<Colon>_", [4, 0], 3)),
- ("_idtyp", typ "id_position => type => idt", Mixfix ("_\\<Colon>_", [], 0)),
- ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\<Colon>_", [], 0)),
("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
(const "Pure.eq", typ "'a => 'a => prop", Infix ("\\<equiv>", 2)),
(const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3\\<And>_./ _)", [0, 0], 0)),