author | paulson |
Thu, 18 Dec 1997 11:13:10 +0100 | |
changeset 4434 | 75f38104ff80 |
parent 4433 | 960868c0cbdd |
child 4435 | 41a7e4f0e957 |
src/HOL/Set.ML | file | annotate | diff | comparison | revisions |
--- 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]);