New example
authorpaulson
Fri Nov 28 10:36:08 1997 +0100 (1997-11-28)
changeset 43225f5df208b0e0
parent 4321 2a2956ccb86c
child 4323 561242f8606b
New example
src/ZF/ex/misc.ML
     1.1 --- a/src/ZF/ex/misc.ML	Fri Nov 28 07:41:24 1997 +0100
     1.2 +++ b/src/ZF/ex/misc.ML	Fri Nov 28 10:36:08 1997 +0100
     1.3 @@ -14,6 +14,11 @@
     1.4  by (Blast_tac 1);
     1.5  result();
     1.6  
     1.7 +(*variant of the benchmark above*)
     1.8 +goal ZF.thy "!!S. ALL x:S. Union(S) <= x ==> EX z. S <= {z}";
     1.9 +by (Blast_tac 1);
    1.10 +result();
    1.11 +
    1.12  context Perm.thy;
    1.13  
    1.14  (*Example 12 (credited to Peter Andrews) from