ex_impE was incorrectly listed as Safe
authorpaulson
Fri Jan 31 17:13:19 1997 +0100 (1997-01-31)
changeset 25728a47f85e7a03
parent 2571 b9f641195b48
child 2573 f3e04805895a
ex_impE was incorrectly listed as Safe
src/FOL/intprover.ML
src/FOLP/intprover.ML
     1.1 --- a/src/FOL/intprover.ML	Fri Jan 31 16:57:45 1997 +0100
     1.2 +++ b/src/FOL/intprover.ML	Fri Jan 31 17:13:19 1997 +0100
     1.3 @@ -42,13 +42,13 @@
     1.4        (false,impI), (false,notI), (false,allI),
     1.5        (true,conjE), (true,exE),
     1.6        (false,conjI), (true,conj_impE),
     1.7 -      (true,disj_impE), (true,ex_impE),
     1.8 -      (true,disjE), (false,iffI), (true,iffE), (true,not_to_imp) ];
     1.9 +      (true,disj_impE), (true,disjE), 
    1.10 +      (false,iffI), (true,iffE), (true,not_to_imp) ];
    1.11  
    1.12  val haz_brls =
    1.13      [ (false,disjI1), (false,disjI2), (false,exI), 
    1.14        (true,allE), (true,not_impE), (true,imp_impE), (true,iff_impE),
    1.15 -      (true,all_impE), (true,impE) ];
    1.16 +      (true,all_impE), (true,ex_impE), (true,impE) ];
    1.17  
    1.18  (*0 subgoals vs 1 or more: the p in safep is for positive*)
    1.19  val (safe0_brls, safep_brls) =
     2.1 --- a/src/FOLP/intprover.ML	Fri Jan 31 16:57:45 1997 +0100
     2.2 +++ b/src/FOLP/intprover.ML	Fri Jan 31 17:13:19 1997 +0100
     2.3 @@ -40,13 +40,13 @@
     2.4        (false,impI), (false,notI), (false,allI),
     2.5        (true,conjE), (true,exE),
     2.6        (false,conjI), (true,conj_impE),
     2.7 -      (true,disj_impE), (true,ex_impE),
     2.8 -      (true,disjE), (false,iffI), (true,iffE), (true,not_to_imp) ];
     2.9 +      (true,disj_impE), (true,disjE), 
    2.10 +      (false,iffI), (true,iffE), (true,not_to_imp) ];
    2.11  
    2.12  val haz_brls =
    2.13      [ (false,disjI1), (false,disjI2), (false,exI), 
    2.14        (true,allE), (true,not_impE), (true,imp_impE), (true,iff_impE),
    2.15 -      (true,all_impE), (true,impE) ];
    2.16 +      (true,all_impE), (true,ex_impE), (true,impE) ];
    2.17  
    2.18  (*0 subgoals vs 1 or more: the p in safep is for positive*)
    2.19  val (safe0_brls, safep_brls) =