| changeset 1532 | 769a4517ad7b |
| parent 1465 | 5d7a7e439cec |
| child 1570 | fd1b9c721ac7 |
--- 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);