# HG changeset patch
# User nipkow
# Date 1144586844 -7200
# Node ID 6cc9ac729eb55ae55c011a16a892c251dbc1e64d
# Parent  1f717bd6b7eaae6f398b911de9a89a24e9511831
Made "empty" an abbreviation.

diff -r 1f717bd6b7ea -r 6cc9ac729eb5 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Sun Apr 09 14:31:37 2006 +0200
+++ b/src/HOL/Map.thy	Sun Apr 09 14:47:24 2006 +0200
@@ -15,6 +15,14 @@
 types ('a,'b) "~=>" = "'a => 'b option" (infixr 0)
 translations (type) "a ~=> b " <= (type) "a => b option"
 
+abbreviation
+  empty     ::  "'a ~=> 'b"
+  "empty == %x. None"
+
+constdefs
+  map_comp :: "('b ~=> 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "o'_m" 55)
+  "f o_m g  == (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
+
 consts
 map_add :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
 restrict_map :: "('a ~=> 'b) => 'a set => ('a ~=> 'b)" (infixl "|`"  110)
@@ -24,16 +32,6 @@
 map_upds:: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)"
 map_le  :: "('a ~=> 'b) => ('a ~=> 'b) => bool" (infix "\<subseteq>\<^sub>m" 50)
 
-constdefs
-  map_comp :: "('b ~=> 'c)  => ('a ~=> 'b) => ('a ~=> 'c)" (infixl "o'_m" 55)
-  "f o_m g  == (\<lambda>k. case g k of None \<Rightarrow> None | Some v \<Rightarrow> f v)"
-
-syntax
-  empty     ::  "'a ~=> 'b"
-translations
-  "empty"    => "%_. None"
-  "empty"    <= "%x. None"
-
 nonterminals
   maplets maplet