# HG changeset patch
# User nipkow
# Date 1049211790 -7200
# Node ID 90611b4e005490c27e3819946c05688be230af73
# Parent  6676ac2527fa8763120308ae99a096150f7233cb
Made empty a translation rather than a constant.

diff -r 6676ac2527fa -r 90611b4e0054 src/HOL/Map.ML
--- a/src/HOL/Map.ML	Tue Apr 01 16:08:34 2003 +0200
+++ b/src/HOL/Map.ML	Tue Apr 01 17:43:10 2003 +0200
@@ -8,17 +8,13 @@
 
 section "empty";
 
-Goalw [empty_def] "empty k = None";
-by (Simp_tac 1);
-qed "empty_def2";
-Addsimps [empty_def2];
-
 Goal "empty(x := None) = empty";
 by (rtac ext 1);
 by (Simp_tac 1);
 qed "empty_upd_none";
 Addsimps [empty_upd_none];
 
+(* FIXME: what is this sum_case nonsense?? *)
 Goal "sum_case empty empty = empty";
 by (rtac ext 1);
 by (simp_tac (simpset() addsplits [sum.split]) 1);
@@ -48,6 +44,7 @@
 qed "finite_range_updI";
 
 
+(* FIXME: what is this sum_case nonsense?? *)
 section "sum_case and empty/map_upd";
 
 Goal "sum_case (m(k|->y)) empty =  (sum_case m empty)(Inl k|->y)";
diff -r 6676ac2527fa -r 90611b4e0054 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Tue Apr 01 16:08:34 2003 +0200
+++ b/src/HOL/Map.thy	Tue Apr 01 17:43:10 2003 +0200
@@ -11,7 +11,6 @@
 types ('a,'b) "~=>" = 'a => 'b option (infixr 0)
 
 consts
-empty	::  "'a ~=> 'b"
 chg_map	:: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)"
 override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
 dom	:: "('a ~=> 'b) => 'a set"
@@ -20,6 +19,7 @@
 map_upds:: "('a ~=> 'b) => 'a list => 'b list => 
 	    ('a ~=> 'b)"			 ("_/'(_[|->]_/')" [900,0,0]900)
 syntax
+empty	::  "'a ~=> 'b"
 map_upd	:: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
 					         ("_/'(_/|->_')"   [900,0,0]900)
 
@@ -31,13 +31,13 @@
 				         ("_/'(_/[\\<mapsto>]/_')" [900,0,0]900)
 
 translations
+  "empty"    => "_K None"
+  "empty"    <= "%x. None"
 
   "m(a|->b)" == "m(a:=Some b)"
 
 defs
 
-empty_def    "empty == %x. None"
-
 chg_map_def  "chg_map f a m == case m a of None => m | Some b => m(a|->f b)"
 
 override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
diff -r 6676ac2527fa -r 90611b4e0054 src/HOL/MicroJava/J/JListExample.thy
--- a/src/HOL/MicroJava/J/JListExample.thy	Tue Apr 01 16:08:34 2003 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy	Tue Apr 01 17:43:10 2003 +0200
@@ -89,7 +89,7 @@
 *}
 
 generate_code
-  test = "example_prg\<turnstile>Norm (Map.empty, Map.empty)
+  test = "example_prg\<turnstile>Norm (empty, empty)
     -(Expr (l1_name::=NewC list_name);;
       Expr ({list_name}(LAcc l1_name)..val_name:=Lit (Intg 1));;
       Expr (l2_name::=NewC list_name);;
diff -r 6676ac2527fa -r 90611b4e0054 src/HOL/W0/W0.thy
--- a/src/HOL/W0/W0.thy	Tue Apr 01 16:08:34 2003 +0200
+++ b/src/HOL/W0/W0.thy	Tue Apr 01 17:43:10 2003 +0200
@@ -133,7 +133,7 @@
   by (rule ext) (simp add: id_subst_def)
 
 lemma dom_id_subst [simp]: "dom id_subst = {}"
-  by (simp add: dom_def id_subst_def empty_def)
+  by (simp add: dom_def id_subst_def)
 
 lemma cod_id_subst [simp]: "cod id_subst = {}"
   by (simp add: cod_def)