src/Provers/quantifier1.ML
changeset 7951 b36913c35699
parent 4319 afb60b8bf15e
child 11221 60c6e91f6079
     1.1 --- a/src/Provers/quantifier1.ML	Wed Oct 27 17:09:31 1999 +0200
     1.2 +++ b/src/Provers/quantifier1.ML	Wed Oct 27 17:17:28 1999 +0200
     1.3 @@ -102,9 +102,10 @@
     1.4            in Some(prove_conv prove_all_tac sg (F,all$Abs(x,T,R))) end)
     1.5    | rearrange_all _ _ _ = None;
     1.6  
     1.7 +(* Better: instantiate exI *)
     1.8  val prove_ex_tac = rtac iffI 1 THEN
     1.9 -    ALLGOALS(EVERY'[etac exE, REPEAT o (etac conjE),
    1.10 -                    rtac exI, REPEAT o (ares_tac [conjI] ORELSE' etac sym)]);
    1.11 +    ALLGOALS(EVERY'[etac exE, REPEAT_DETERM o (etac conjE), rtac exI,
    1.12 +                    DEPTH_SOLVE_1 o (ares_tac [conjI] APPEND' etac sym)]);
    1.13  
    1.14  fun rearrange_ex sg _ (F as ex $ Abs(x,T,P)) =
    1.15       (case extract P of