| changeset 4109 | b131edcfeac3 |
| parent 4089 | 96fba19bcbe2 |
| child 4153 | e534c4c32d54 |
--- a/src/HOL/ex/set.ML Mon Nov 03 21:56:59 1997 +0100 +++ b/src/HOL/ex/set.ML Tue Nov 04 09:26:15 1997 +0100 @@ -9,7 +9,7 @@ writeln"File HOL/ex/set."; -set_current_thy"Set"; +context Set.thy; (*Nice demonstration of blast_tac--and its overloading problems*) goal Set.thy "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";