--- a/src/HOLCF/IOA/ABP/Correctness.ML Fri Oct 24 11:05:21 1997 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.ML Fri Oct 24 11:24:21 1997 +0200
@@ -254,8 +254,6 @@
by (ALLGOALS (simp_tac ((!simpset addsimps [externals_def]) setloop (split_tac [expand_if]))));
qed"env_unchanged";
-Delsimps [Collect_False_empty];
-
goal Correctness.thy "compatible srch_ioa rsch_ioa";
by (simp_tac (!simpset addsimps [compatible_def,Int_def,empty_def]) 1);
by (rtac set_ext 1);
@@ -381,4 +379,4 @@
qed "system_refinement";
-*)
\ No newline at end of file
+*)