# HG changeset patch
# User nipkow
# Date 877685061 -7200
# Node ID 93ca73409df3be7346955ea2bc37a6387d8b3e46
# Parent  2a903ba8d39e7222f516e45925533e9a0f5374a4
Deleted very odd Delsimps[Collect_False_empty] which made proofs fail!

diff -r 2a903ba8d39e -r 93ca73409df3 src/HOLCF/IOA/ABP/Correctness.ML
--- 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
+*)