# HG changeset patch
# User nipkow
# Date 901293495 -7200
# Node ID 277831ae7eac3b4c603d8ba49eb168aeab0e04b4
# Parent  650bf0ce02298c23d2aaa7144fc81b9eca7e23fe
Map.update -> map_upd, Unpdate.update -> fun_upd
Problem: macros get confused about two updates.

diff -r 650bf0ce0229 -r 277831ae7eac src/HOL/Map.ML
--- a/src/HOL/Map.ML	Fri Jul 24 14:53:23 1998 +0200
+++ b/src/HOL/Map.ML	Fri Jul 24 17:18:15 1998 +0200
@@ -11,28 +11,28 @@
 qed "empty_def2";
 Addsimps [empty_def2];
 
-Goalw [update_def] "(m[a|->b])x = (if x=a then Some b else m x)";
+Goalw [map_upd_def] "(m[a|->b])x = (if x=a then Some b else m x)";
 by (Simp_tac 1);
-qed "update_def2";
-Addsimps [update_def2];
+qed "map_upd_def2";
+Addsimps [map_upd_def2];
 
-qed_goal "update_same" thy "(t[k|->x]) k = Some x" 
+qed_goal "map_upd_same" thy "(t[k|->x]) k = Some x" 
 	(K [Simp_tac 1]);
-qed_goal "update_other" thy "!!X. l~=k ==> (t[k|->x]) l = t l"
+qed_goal "map_upd_other" thy "!!X. l~=k ==> (t[k|->x]) l = t l"
 	(K [Asm_simp_tac 1]);
-qed_goal "update_triv" thy "!!X. t k = Some x ==> t[k|->x] = t"
+qed_goal "map_upd_triv" thy "!!X. t k = Some x ==> t[k|->x] = t"
 	(K [rtac ext 1, Asm_simp_tac 1]);
-(*Addsimps [update_same, update_other, update_triv];*)
+(*Addsimps [map_upd_same, map_upd_other, map_upd_triv];*)
 
 section "option_map";
 
 qed_goal "option_map_o_empty" thy 
          "option_map f o empty = empty" (K [rtac ext 1, Simp_tac 1]);
 
-qed_goal "option_map_o_update" thy 
+qed_goal "option_map_o_map_upd" thy 
 	 "option_map f o m[a|->b] = (option_map f o m)[a|->f b]" 
 	(K [rtac ext 1, Simp_tac 1]);
-Addsimps[option_map_o_empty, option_map_o_update];
+Addsimps[option_map_o_empty, option_map_o_map_upd];
 
 section "++";
 
@@ -87,8 +87,8 @@
 Goalw [dom_def] "dom(m[a|->b]) = insert a (dom m)";
 by (Simp_tac 1);
 by (Blast_tac 1);
-qed "dom_update";
-Addsimps [dom_update];
+qed "dom_map_upd";
+Addsimps [dom_map_upd];
 
 qed_goalw "finite_dom_map_of" Map.thy [dom_def] "finite (dom (map_of l))" (K[
 	induct_tac "l" 1,
@@ -112,5 +112,5 @@
 by Auto_tac;
 by (subgoal_tac "~(aa = a)" 1);
 by Auto_tac;
-qed "ran_update";
-Addsimps [ran_update];
+qed "ran_map_upd";
+Addsimps [ran_map_upd];
diff -r 650bf0ce0229 -r 277831ae7eac src/HOL/Map.thy
--- a/src/HOL/Map.thy	Fri Jul 24 14:53:23 1998 +0200
+++ b/src/HOL/Map.thy	Fri Jul 24 17:18:15 1998 +0200
@@ -12,7 +12,7 @@
 
 consts
 empty   :: "'a ~=> 'b"
-update  :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
+map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
            ("_/[_/|->/_]" [900,0,0] 900)
 override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100)
 dom     :: "('a ~=> 'b) => 'a set"
@@ -22,7 +22,7 @@
 syntax (symbols)
   "~=>"     :: [type, type] => type
                (infixr "\\<leadsto>" 0)
-  update    :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
+  map_upd    :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)"
                ("_/[_/\\<mapsto>/_]" [900,0,0] 900)
   override  :: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)"
                (infixl "\\<oplus>" 100)
@@ -30,7 +30,7 @@
 defs
 empty_def "empty == %x. None"
 
-update_def "m[a|->b] == %x. if x=a then Some b else m x"
+map_upd_def "m[a|->b] == %x. if x=a then Some b else m x"
 
 override_def "m1++m2 == %x. case m2 x of None => m1 x | Some y => Some y"
 
diff -r 650bf0ce0229 -r 277831ae7eac src/HOL/Update.ML
--- a/src/HOL/Update.ML	Fri Jul 24 14:53:23 1998 +0200
+++ b/src/HOL/Update.ML	Fri Jul 24 17:18:15 1998 +0200
@@ -8,20 +8,20 @@
 
 open Update;
 
-Goalw [update_def] "(f(x:=y) = f) = (f x = y)";
+Goalw [fun_upd_def] "(f(x:=y) = f) = (f x = y)";
 by Safe_tac;
 by (etac subst 1);
 by (rtac ext 2);
 by Auto_tac;
-qed "update_idem_iff";
+qed "fun_upd_idem_iff";
 
 (* f x = y ==> f(x:=y) = f *)
-bind_thm("update_idem", update_idem_iff RS iffD2);
+bind_thm("fun_upd_idem", fun_upd_idem_iff RS iffD2);
 
 (* f(x := f x) = f *)
-AddIffs [refl RS update_idem];
+AddIffs [refl RS fun_upd_idem];
 
 Goal "(f(x:=y))z = (if z=x then y else f z)";
-by (simp_tac (simpset() addsimps [update_def]) 1);
-qed "update_apply";
-Addsimps [update_apply];
+by (simp_tac (simpset() addsimps [fun_upd_def]) 1);
+qed "fun_upd_apply";
+Addsimps [fun_upd_apply];
diff -r 650bf0ce0229 -r 277831ae7eac src/HOL/Update.thy
--- a/src/HOL/Update.thy	Fri Jul 24 14:53:23 1998 +0200
+++ b/src/HOL/Update.thy	Fri Jul 24 17:18:15 1998 +0200
@@ -9,7 +9,7 @@
 Update = Fun +
 
 consts
-  update  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
+  fun_upd  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
 
 nonterminals
   updbinds  updbind
@@ -25,9 +25,9 @@
 
 translations
   "_Update f (_updbinds b bs)"  == "_Update (_Update f b) bs"
-  "f(x:=y)"                     == "update f x y"
+  "f(x:=y)"                     == "fun_upd f x y"
 
 defs
-  update_def "f(a:=b) == %x. if x=a then b else f x"
+  fun_upd_def "f(a:=b) == %x. if x=a then b else f x"
 
 end