# HG changeset patch
# User wenzelm
# Date 933883903 -7200
# Node ID 6ffe5067d5cc4d44d3fd93b89f92bd705570e6ab
# Parent  50b9849cf6adb18440054978c0026eaa075efebf
removed obsolete addsimps update_defs;

diff -r 50b9849cf6ad -r 6ffe5067d5cc src/HOL/UNITY/Client.ML
--- a/src/HOL/UNITY/Client.ML	Thu Aug 05 22:11:07 1999 +0200
+++ b/src/HOL/UNITY/Client.ML	Thu Aug 05 22:11:43 1999 +0200
@@ -12,9 +12,6 @@
 
 Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]);
 
-(*Simplification for records*)
-Addsimps (thms"state.update_defs");
-
 
 fun invariant_tac i = 
     rtac invariantI i  THEN
diff -r 50b9849cf6ad -r 6ffe5067d5cc src/HOL/UNITY/Handshake.ML
--- a/src/HOL/UNITY/Handshake.ML	Thu Aug 05 22:11:07 1999 +0200
+++ b/src/HOL/UNITY/Handshake.ML	Thu Aug 05 22:11:43 1999 +0200
@@ -15,9 +15,6 @@
 program_defs_ref := [F_def, G_def];
 
 Addsimps (map simp_of_act [cmdF_def, cmdG_def]);
-
-(*Simplification for records*)
-Addsimps (thms"state.update_defs");
 Addsimps [simp_of_set invFG_def];
 
 
diff -r 50b9849cf6ad -r 6ffe5067d5cc src/HOL/UNITY/Lift.ML
--- a/src/HOL/UNITY/Lift.ML	Thu Aug 05 22:11:07 1999 +0200
+++ b/src/HOL/UNITY/Lift.ML	Thu Aug 05 22:11:43 1999 +0200
@@ -60,9 +60,6 @@
 (* [| Lift: B LeadsTo C; Lift: A LeadsTo B |] ==> Lift: (A Un B) LeadsTo C *)
 
 
-(*Simplification for records*)
-Addsimps (thms"state.update_defs");
-
 Addsimps [bounded_def, open_stop_def, open_move_def, stop_floor_def,
 	  moving_up_def, moving_down_def];
 
diff -r 50b9849cf6ad -r 6ffe5067d5cc src/HOL/UNITY/Mutex.ML
--- a/src/HOL/UNITY/Mutex.ML	Thu Aug 05 22:11:07 1999 +0200
+++ b/src/HOL/UNITY/Mutex.ML	Thu Aug 05 22:11:43 1999 +0200
@@ -18,8 +18,6 @@
 
 Addsimps (map simp_of_set [IU_def, IV_def, bad_IU_def]);
 
-(*Simplification for records*)
-Addsimps (thms"state.update_defs");
 
 Goal "Mutex : Always IU";
 by (rtac AlwaysI 1);