--- 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
--- 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];
--- 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];
--- 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);