src/HOL/ex/set.ML
changeset 4153 e534c4c32d54
parent 4109 b131edcfeac3
child 4324 9bfac4684f2f
     1.1 --- a/src/HOL/ex/set.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/ex/set.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -9,15 +9,14 @@
     1.4  
     1.5  writeln"File HOL/ex/set.";
     1.6  
     1.7 -context Set.thy;
     1.8 +context Lfp.thy;
     1.9  
    1.10 -(*Nice demonstration of blast_tac--and its overloading problems*)
    1.11 +(*Nice demonstration of blast_tac--and its limitations*)
    1.12  goal Set.thy "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
    1.13 -let val insertCI' = read_instantiate [("'a", "?'a set")] insertCI
    1.14 -in    (*Type instantiation is required so that blast_tac can apply equalityI
    1.15 -        to the subgoal arising from insertCI*)
    1.16 -by(blast_tac (claset() addSIs [insertCI']) 1)
    1.17 -end;
    1.18 +(*for some unfathomable reason, UNIV_I increases the search space greatly*)
    1.19 +by (blast_tac (claset() delrules [UNIV_I]) 1);
    1.20 +result();
    1.21 +
    1.22  
    1.23  (*** A unique fixpoint theorem --- fast/best/meson all fail ***)
    1.24