--- a/NEWS Mon Aug 31 20:56:24 2015 +0200
+++ b/NEWS Mon Aug 31 21:01:21 2015 +0200
@@ -181,6 +181,14 @@
*** HOL ***
+* Some old and rarely used ASCII replacement syntax has been removed.
+INCOMPATIBILITY, standard syntax with symbols should be used instead.
+The subsequent commands help to reproduce the old forms, e.g. to
+simplify porting old theories:
+
+ type_notation Map.map (infixr "~=>" 0)
+ notation Map.map_comp (infixl "o'_m" 55)
+
* Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has
been removed. INCOMPATIBILITY.
--- a/src/HOL/Bali/Table.thy Mon Aug 31 20:56:24 2015 +0200
+++ b/src/HOL/Bali/Table.thy Mon Aug 31 21:01:21 2015 +0200
@@ -361,7 +361,7 @@
(*###TO Map?*)
-primrec atleast_free :: "('a ~=> 'b) => nat => bool"
+primrec atleast_free :: "('a \<rightharpoonup> 'b) => nat => bool"
where
"atleast_free m 0 = True"
| atleast_free_Suc: "atleast_free m (Suc n) = (\<exists>a. m a = None & (!b. atleast_free (m(a|->b)) n))"
--- a/src/HOL/IMPP/Com.thy Mon Aug 31 20:56:24 2015 +0200
+++ b/src/HOL/IMPP/Com.thy Mon Aug 31 21:01:21 2015 +0200
@@ -43,7 +43,7 @@
consts bodies :: "(pname * com) list"(* finitely many procedure definitions *)
definition
- body :: " pname ~=> com" where
+ body :: " pname \<rightharpoonup> com" where
"body = map_of bodies"
--- a/src/HOL/Map.thy Mon Aug 31 20:56:24 2015 +0200
+++ b/src/HOL/Map.thy Mon Aug 31 21:01:21 2015 +0200
@@ -11,21 +11,15 @@
imports List
begin
-type_synonym ('a, 'b) "map" = "'a \<Rightarrow> 'b option" (infixr "~=>" 0)
-
-type_notation (xsymbols)
- "map" (infixr "\<rightharpoonup>" 0)
+type_synonym ('a, 'b) "map" = "'a \<Rightarrow> 'b option" (infixr "\<rightharpoonup>" 0)
abbreviation
empty :: "'a \<rightharpoonup> 'b" where
"empty \<equiv> \<lambda>x. None"
definition
- map_comp :: "('b \<rightharpoonup> 'c) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'c)" (infixl "o'_m" 55) where
- "f o_m g = (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
-
-notation (xsymbols)
- map_comp (infixl "\<circ>\<^sub>m" 55)
+ map_comp :: "('b \<rightharpoonup> 'c) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'c)" (infixl "\<circ>\<^sub>m" 55) where
+ "f \<circ>\<^sub>m g = (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
definition
map_add :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" (infixl "++" 100) where
--- a/src/HOL/Nominal/Examples/Fsub.thy Mon Aug 31 20:56:24 2015 +0200
+++ b/src/HOL/Nominal/Examples/Fsub.thy Mon Aug 31 21:01:21 2015 +0200
@@ -17,7 +17,7 @@
section {* Types for Names, Nominal Datatype Declaration for Types and Terms *}
no_syntax
- "_Map" :: "maplets => 'a ~=> 'b" ("(1[_])")
+ "_Map" :: "maplets => 'a \<rightharpoonup> 'b" ("(1[_])")
text {* The main point of this solution is to use names everywhere (be they bound,
binding or free). In System \FSUB{} there are two kinds of names corresponding to
--- a/src/HOL/Nominal/Examples/Pattern.thy Mon Aug 31 20:56:24 2015 +0200
+++ b/src/HOL/Nominal/Examples/Pattern.thy Mon Aug 31 21:01:21 2015 +0200
@@ -5,7 +5,7 @@
begin
no_syntax
- "_Map" :: "maplets => 'a ~=> 'b" ("(1[_])")
+ "_Map" :: "maplets => 'a \<rightharpoonup> 'b" ("(1[_])")
atom_decl name