UNIV_I no longer counts as safe
authorpaulson
Thu, 18 Dec 1997 11:13:10 +0100
changeset 4434 75f38104ff80
parent 4433 960868c0cbdd
child 4435 41a7e4f0e957
UNIV_I no longer counts as safe
src/HOL/Set.ML
--- a/src/HOL/Set.ML	Wed Dec 17 18:13:43 1997 +0100
+++ b/src/HOL/Set.ML	Thu Dec 18 11:13:10 1997 +0100
@@ -216,7 +216,8 @@
 qed_goalw "UNIV_I" Set.thy [UNIV_def] "x : UNIV"
   (fn _ => [rtac CollectI 1, rtac TrueI 1]);
 
-AddIffs [UNIV_I];
+Addsimps [UNIV_I];
+AddIs    [UNIV_I];  (*unsafe makes it less likely to cause problems*)
 
 qed_goal "subset_UNIV" Set.thy "A <= UNIV"
   (fn _ => [rtac subsetI 1, rtac UNIV_I 1]);