src/HOL/UNITY/Extend.ML
changeset 11467 1064effe37f6
parent 11170 015af2fc7026
child 12338 de0f4a63baa5
     1.1 --- a/src/HOL/UNITY/Extend.ML	Mon Aug 06 15:54:29 2001 +0200
     1.2 +++ b/src/HOL/UNITY/Extend.ML	Mon Aug 06 16:43:40 2001 +0200
     1.3 @@ -753,14 +753,11 @@
     1.4  by (auto_tac (claset(), simpset() addsimps [ok_def]));  
     1.5  qed "ok_extend_iff";
     1.6  
     1.7 -Unify.search_bound := 40;
     1.8 -Unify.trace_bound  := 40;
     1.9 -
    1.10 -Goal "OK I (%i. extend h (F i)) = (OK I F)";
    1.11 -by (auto_tac (claset(), simpset() addsimps [OK_def]));  
    1.12 +Goalw [OK_def] "OK I (%i. extend h (F i)) = (OK I F)";
    1.13 +by Safe_tac;
    1.14  by (dres_inst_tac [("x","i")] bspec 1); 
    1.15 -by (dres_inst_tac [("x","j")] bspec 2); 
    1.16 -by Auto_tac;  
    1.17 +by (dres_inst_tac [("x","j")] bspec 2);  
    1.18 +by (REPEAT (Force_tac 1));
    1.19  qed "OK_extend_iff";
    1.20  
    1.21  Goal "F : X guarantees Y ==> \