src/FOLP/intprover.ML
changeset 26322 eaf634e975fa
parent 24584 01e83ffa6c54
child 35762 af3ff2ba4c54
     1.1 --- a/src/FOLP/intprover.ML	Tue Mar 18 21:57:36 2008 +0100
     1.2 +++ b/src/FOLP/intprover.ML	Tue Mar 18 22:19:18 2008 +0100
     1.3 @@ -36,17 +36,17 @@
     1.4    step of an intuitionistic proof.
     1.5  *)
     1.6  val safe_brls = sort (make_ord lessb)
     1.7 -    [ (true,FalseE), (false,TrueI), (false,refl),
     1.8 -      (false,impI), (false,notI), (false,allI),
     1.9 -      (true,conjE), (true,exE),
    1.10 -      (false,conjI), (true,conj_impE),
    1.11 -      (true,disj_impE), (true,disjE), 
    1.12 -      (false,iffI), (true,iffE), (true,not_to_imp) ];
    1.13 +    [ (true, @{thm FalseE}), (false, @{thm TrueI}), (false, @{thm refl}),
    1.14 +      (false, @{thm impI}), (false, @{thm notI}), (false, @{thm allI}),
    1.15 +      (true, @{thm conjE}), (true, @{thm exE}),
    1.16 +      (false, @{thm conjI}), (true, @{thm conj_impE}),
    1.17 +      (true, @{thm disj_impE}), (true, @{thm disjE}), 
    1.18 +      (false, @{thm iffI}), (true, @{thm iffE}), (true, @{thm not_to_imp}) ];
    1.19  
    1.20  val haz_brls =
    1.21 -    [ (false,disjI1), (false,disjI2), (false,exI), 
    1.22 -      (true,allE), (true,not_impE), (true,imp_impE), (true,iff_impE),
    1.23 -      (true,all_impE), (true,ex_impE), (true,impE) ];
    1.24 +    [ (false, @{thm disjI1}), (false, @{thm disjI2}), (false, @{thm exI}), 
    1.25 +      (true, @{thm allE}), (true, @{thm not_impE}), (true, @{thm imp_impE}), (true, @{thm iff_impE}),
    1.26 +      (true, @{thm all_impE}), (true, @{thm ex_impE}), (true, @{thm impE}) ];
    1.27  
    1.28  (*0 subgoals vs 1 or more: the p in safep is for positive*)
    1.29  val (safe0_brls, safep_brls) =
    1.30 @@ -76,4 +76,3 @@
    1.31    SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, size_of_thm) (step_tac 1));
    1.32  
    1.33  end;
    1.34 -