# HG changeset patch
# User nipkow
# Date 825946710 -3600
# Node ID 769a4517ad7bbc92ea63635e9d776859ee2d590d
# Parent  e5eb247ad13c06159ce2462aac7ab0890ec37ccd
Proof modification.

diff -r e5eb247ad13c -r 769a4517ad7b src/HOL/IOA/ABP/Correctness.ML
--- a/src/HOL/IOA/ABP/Correctness.ML	Mon Mar 04 14:37:33 1996 +0100
+++ b/src/HOL/IOA/ABP/Correctness.ML	Mon Mar 04 14:38:30 1996 +0100
@@ -270,6 +270,7 @@
 by (ALLGOALS (simp_tac ((!simpset addsimps [externals_def]) setloop (split_tac [expand_if]))));
 qed"env_unchanged";
 
+Delsimps [Collect_False_empty];
 
 goal Correctness.thy "compat_ioas srch_ioa rsch_ioa"; 
 by (simp_tac (!simpset addsimps [compat_ioas_def,compat_asigs_def,Int_def,empty_def]) 1);