# HG changeset patch
# User nipkow
# Date 901293655 -7200
# Node ID 1dd4ec921f710a860233b01898fcc00a4523f30e
# Parent  277831ae7eac3b4c603d8ba49eb168aeab0e04b4
update -> fun_upd

diff -r 277831ae7eac -r 1dd4ec921f71 src/HOL/UNITY/Reach.ML
--- a/src/HOL/UNITY/Reach.ML	Fri Jul 24 17:18:15 1998 +0200
+++ b/src/HOL/UNITY/Reach.ML	Fri Jul 24 17:20:55 1998 +0200
@@ -21,7 +21,7 @@
 AddSEs [ifE];
 
 
-val cmd_defs = [racts_def, asgt_def, update_def];
+val cmd_defs = [racts_def, asgt_def, fun_upd_def];
 
 Goalw [racts_def] "id : racts";
 by (Simp_tac 1);
@@ -117,13 +117,13 @@
 	      ([Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym, 
 		racts_def, asgt_def])) 1);
 by Safe_tac;
-by (rtac update_idem 1);
+by (rtac fun_upd_idem 1);
 by (Blast_tac 1);
 by (Full_simp_tac 1);
 by (REPEAT (dtac bspec 1 THEN Simp_tac 1));
 by (dtac subsetD 1);
 by (Simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [update_idem_iff]) 1);
+by (asm_full_simp_tac (simpset() addsimps [fun_upd_idem_iff]) 1);
 qed "Compl_fixedpoint";
 
 Goal "A - fixedpoint = (UN (u,v): edges. A Int {s. s u & ~ s v})";
@@ -149,7 +149,7 @@
 Goal "metric (s(y:=s x | s y)) <= metric s";
 by (case_tac "s x --> s y" 1);
 by (auto_tac (claset() addIs [less_imp_le],
-	      simpset() addsimps [update_idem]));
+	      simpset() addsimps [fun_upd_idem]));
 qed "metric_le";
 
 Goal "(u,v): edges ==> \