--- a/src/HOL/UNITY/Handshake.ML Mon Aug 16 18:43:13 1999 +0200
+++ b/src/HOL/UNITY/Handshake.ML Mon Aug 16 18:47:20 1999 +0200
@@ -8,9 +8,6 @@
From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
*)
-(*split_all_tac causes a big blow-up*)
-claset_ref() := claset() delSWrapper record_split_name;
-
Addsimps [F_def RS def_prg_Init, G_def RS def_prg_Init];
program_defs_ref := [F_def, G_def];
--- a/src/HOL/UNITY/Lift.ML Mon Aug 16 18:43:13 1999 +0200
+++ b/src/HOL/UNITY/Lift.ML Mon Aug 16 18:47:20 1999 +0200
@@ -6,9 +6,6 @@
The Lift-Control Example
*)
-(*split_all_tac causes a big blow-up*)
-claset_ref() := claset() delSWrapper record_split_name;
-
Goal "[| x ~: A; y : A |] ==> x ~= y";
by (Blast_tac 1);
qed "not_mem_distinct";
--- a/src/HOL/UNITY/Mutex.ML Mon Aug 16 18:43:13 1999 +0200
+++ b/src/HOL/UNITY/Mutex.ML Mon Aug 16 18:47:20 1999 +0200
@@ -6,9 +6,6 @@
Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
*)
-(*record_split_name causes a BIG blow-up (doubles the run-time)*)
-claset_ref() := claset() delSWrapper record_split_name;
-
Addsimps [Mutex_def RS def_prg_Init];
program_defs_ref := [Mutex_def];