Deleted very odd Delsimps[Collect_False_empty] which made proofs fail!
authornipkow
Fri, 24 Oct 1997 11:24:21 +0200
changeset 3983 93ca73409df3
parent 3982 2a903ba8d39e
child 3984 8fc76a487616
Deleted very odd Delsimps[Collect_False_empty] which made proofs fail!
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
+*)