# HG changeset patch # User wenzelm # Date 1441802861 -7200 # Node ID 5f898411ce87c8f3b6e94228980deb62f9eb8452 # Parent 6d29eb7c5fb283be8cd68cb307a94429ca25d12d eliminated \ from syntax of constraints; diff -r 6d29eb7c5fb2 -r 5f898411ce87 NEWS --- 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 "\" 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 diff -r 6d29eb7c5fb2 -r 5f898411ce87 src/Doc/Codegen/Setup.thy --- 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 \ -let - val typ = Simple_Syntax.read_typ; -in - Sign.del_syntax (Symbol.xsymbolsN, false) - [("_constrain", typ "logic => type => logic", Mixfix ("_\_", [4, 0], 3)), - ("_constrain", typ "prop' => type => prop'", Mixfix ("_\_", [4, 0], 3))] #> - Sign.add_syntax (Symbol.xsymbolsN, false) - [("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), - ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \ _", [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) declare [[default_code_width = 74]] diff -r 6d29eb7c5fb2 -r 5f898411ce87 src/Doc/Isar_Ref/Inner_Syntax.thy --- 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 "\"}, - which actually looks exactly the same in some {\LaTeX} styles. - \item Dummy variables (written as underscore) may occur in different roles. diff -r 6d29eb7c5fb2 -r 5f898411ce87 src/HOL/Imperative_HOL/Overview.thy --- 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 ("_\_", [4, 0], 3)), - ("_constrain", typ "prop' => type => prop'", Mixfix ("_\_", [4, 0], 3))] #> - Sign.add_syntax (Symbol.xsymbolsN, false) - [("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), - ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \ _", [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 diff -r 6d29eb7c5fb2 -r 5f898411ce87 src/HOL/Library/OptionalSugar.thy --- 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" ("_\_" [4, 0] 3) - "_constrain" :: "prop' => type => prop'" ("_\_" [4, 0] 3) - -syntax (xsymbols 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) (* sorts as intersections *) diff -r 6d29eb7c5fb2 -r 5f898411ce87 src/HOL/SPARK/Manual/Reference.thy --- 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" ("_ \ _" [4, 0] 3) + "_constrain" :: "logic => type => logic" ("_ :: _" [4, 0] 3) (*>*) chapter {* HOL-\SPARK{} Reference *} diff -r 6d29eb7c5fb2 -r 5f898411ce87 src/Pure/pure_thy.ML --- 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 ("(_/ \\ _)", [1, 0], 0)), ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\ _)", [0, 0], 0)), - ("_ofsort", typ "tid_position => sort => type", Mixfix ("_\\_", [1000, 0], 1000)), - ("_constrain", typ "logic => type => logic", Mixfix ("_\\_", [4, 0], 3)), - ("_constrain", typ "prop' => type => prop'", Mixfix ("_\\_", [4, 0], 3)), - ("_idtyp", typ "id_position => type => idt", Mixfix ("_\\_", [], 0)), - ("_idtypdummy", typ "type => idt", Mixfix ("'_()\\_", [], 0)), ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\_./ _)", [0, 3], 3)), (const "Pure.eq", typ "'a => 'a => prop", Infix ("\\", 2)), (const "Pure.all_binder", typ "idts => prop => prop", Mixfix ("(3\\_./ _)", [0, 0], 0)),