prefer symbols;
authorwenzelm
Mon Aug 31 21:01:21 2015 +0200 (2015-08-31)
changeset 61069aefe89038dd2
parent 61068 6cb92c2a5ece
child 61070 b72a990adfe2
prefer symbols;
NEWS
src/HOL/Bali/Table.thy
src/HOL/IMPP/Com.thy
src/HOL/Map.thy
src/HOL/Nominal/Examples/Fsub.thy
src/HOL/Nominal/Examples/Pattern.thy
     1.1 --- a/NEWS	Mon Aug 31 20:56:24 2015 +0200
     1.2 +++ b/NEWS	Mon Aug 31 21:01:21 2015 +0200
     1.3 @@ -181,6 +181,14 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Some old and rarely used ASCII replacement syntax has been removed.
     1.8 +INCOMPATIBILITY, standard syntax with symbols should be used instead.
     1.9 +The subsequent commands help to reproduce the old forms, e.g. to
    1.10 +simplify porting old theories:
    1.11 +
    1.12 +  type_notation Map.map  (infixr "~=>" 0)
    1.13 +  notation Map.map_comp  (infixl "o'_m" 55)
    1.14 +
    1.15  * Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has
    1.16  been removed. INCOMPATIBILITY.
    1.17  
     2.1 --- a/src/HOL/Bali/Table.thy	Mon Aug 31 20:56:24 2015 +0200
     2.2 +++ b/src/HOL/Bali/Table.thy	Mon Aug 31 21:01:21 2015 +0200
     2.3 @@ -361,7 +361,7 @@
     2.4  
     2.5  
     2.6  (*###TO Map?*)
     2.7 -primrec atleast_free :: "('a ~=> 'b) => nat => bool"
     2.8 +primrec atleast_free :: "('a \<rightharpoonup> 'b) => nat => bool"
     2.9  where
    2.10    "atleast_free m 0 = True"
    2.11  | atleast_free_Suc: "atleast_free m (Suc n) = (\<exists>a. m a = None & (!b. atleast_free (m(a|->b)) n))"
     3.1 --- a/src/HOL/IMPP/Com.thy	Mon Aug 31 20:56:24 2015 +0200
     3.2 +++ b/src/HOL/IMPP/Com.thy	Mon Aug 31 21:01:21 2015 +0200
     3.3 @@ -43,7 +43,7 @@
     3.4  
     3.5  consts bodies :: "(pname  *  com) list"(* finitely many procedure definitions *)
     3.6  definition
     3.7 -  body :: " pname ~=> com" where
     3.8 +  body :: " pname \<rightharpoonup> com" where
     3.9    "body = map_of bodies"
    3.10  
    3.11  
     4.1 --- a/src/HOL/Map.thy	Mon Aug 31 20:56:24 2015 +0200
     4.2 +++ b/src/HOL/Map.thy	Mon Aug 31 21:01:21 2015 +0200
     4.3 @@ -11,21 +11,15 @@
     4.4  imports List
     4.5  begin
     4.6  
     4.7 -type_synonym ('a, 'b) "map" = "'a \<Rightarrow> 'b option" (infixr "~=>" 0)
     4.8 -
     4.9 -type_notation (xsymbols)
    4.10 -  "map" (infixr "\<rightharpoonup>" 0)
    4.11 +type_synonym ('a, 'b) "map" = "'a \<Rightarrow> 'b option" (infixr "\<rightharpoonup>" 0)
    4.12  
    4.13  abbreviation
    4.14    empty :: "'a \<rightharpoonup> 'b" where
    4.15    "empty \<equiv> \<lambda>x. None"
    4.16  
    4.17  definition
    4.18 -  map_comp :: "('b \<rightharpoonup> 'c) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'c)"  (infixl "o'_m" 55) where
    4.19 -  "f o_m g = (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
    4.20 -
    4.21 -notation (xsymbols)
    4.22 -  map_comp  (infixl "\<circ>\<^sub>m" 55)
    4.23 +  map_comp :: "('b \<rightharpoonup> 'c) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'c)"  (infixl "\<circ>\<^sub>m" 55) where
    4.24 +  "f \<circ>\<^sub>m g = (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
    4.25  
    4.26  definition
    4.27    map_add :: "('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)"  (infixl "++" 100) where
     5.1 --- a/src/HOL/Nominal/Examples/Fsub.thy	Mon Aug 31 20:56:24 2015 +0200
     5.2 +++ b/src/HOL/Nominal/Examples/Fsub.thy	Mon Aug 31 21:01:21 2015 +0200
     5.3 @@ -17,7 +17,7 @@
     5.4  section {* Types for Names, Nominal Datatype Declaration for Types and Terms *}
     5.5  
     5.6  no_syntax
     5.7 -  "_Map" :: "maplets => 'a ~=> 'b"  ("(1[_])")
     5.8 +  "_Map" :: "maplets => 'a \<rightharpoonup> 'b"  ("(1[_])")
     5.9  
    5.10  text {* The main point of this solution is to use names everywhere (be they bound, 
    5.11    binding or free). In System \FSUB{} there are two kinds of names corresponding to 
     6.1 --- a/src/HOL/Nominal/Examples/Pattern.thy	Mon Aug 31 20:56:24 2015 +0200
     6.2 +++ b/src/HOL/Nominal/Examples/Pattern.thy	Mon Aug 31 21:01:21 2015 +0200
     6.3 @@ -5,7 +5,7 @@
     6.4  begin
     6.5  
     6.6  no_syntax
     6.7 -  "_Map" :: "maplets => 'a ~=> 'b"  ("(1[_])")
     6.8 +  "_Map" :: "maplets => 'a \<rightharpoonup> 'b"  ("(1[_])")
     6.9  
    6.10  atom_decl name
    6.11