# HG changeset patch
# User wenzelm
# Date 1441047681 -7200
# Node ID aefe89038dd288e9ca985c3a79b46f351d38fcdb
# Parent  6cb92c2a5ece5ad3bd5c1384a35ace47d718cf82
prefer symbols;

diff -r 6cb92c2a5ece -r aefe89038dd2 NEWS
--- 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.
 
diff -r 6cb92c2a5ece -r aefe89038dd2 src/HOL/Bali/Table.thy
--- 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))"
diff -r 6cb92c2a5ece -r aefe89038dd2 src/HOL/IMPP/Com.thy
--- 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"
 
 
diff -r 6cb92c2a5ece -r aefe89038dd2 src/HOL/Map.thy
--- 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
diff -r 6cb92c2a5ece -r aefe89038dd2 src/HOL/Nominal/Examples/Fsub.thy
--- 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 
diff -r 6cb92c2a5ece -r aefe89038dd2 src/HOL/Nominal/Examples/Pattern.thy
--- 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