src/HOL/Map.thy
changeset 21210 c17fd2df4e9e
parent 20800 69c82605efcf
child 21404 eb85850d3eb7
     1.1 --- a/src/HOL/Map.thy	Tue Nov 07 11:47:56 2006 +0100
     1.2 +++ b/src/HOL/Map.thy	Tue Nov 07 11:47:57 2006 +0100
     1.3 @@ -26,7 +26,7 @@
     1.4    map_comp :: "('b ~=> 'c)  => ('a ~=> 'b) => ('a ~=> 'c)"  (infixl "o'_m" 55)
     1.5    "f o_m g = (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
     1.6  
     1.7 -const_syntax (xsymbols)
     1.8 +notation (xsymbols)
     1.9    map_comp  (infixl "\<circ>\<^sub>m" 55)
    1.10  
    1.11  definition
    1.12 @@ -36,7 +36,7 @@
    1.13    restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)"  (infixl "|`"  110)
    1.14    "m|`A = (\<lambda>x. if x : A then m x else None)"
    1.15  
    1.16 -const_syntax (latex output)
    1.17 +notation (latex output)
    1.18    restrict_map  ("_\<restriction>\<^bsub>_\<^esub>" [111,110] 110)
    1.19  
    1.20  definition