src/HOL/simpdata.ML
changeset 2443 a81d4c219c3c
parent 2263 c741309167bf
child 2595 548f8ed89a80
     1.1 --- a/src/HOL/simpdata.ML	Wed Dec 18 15:11:07 1996 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Wed Dec 18 15:12:34 1996 +0100
     1.3 @@ -307,11 +307,17 @@
     1.4     ("All", [spec]), ("True", []), ("False", []),
     1.5     ("If", [if_bool_eq RS iffD1])];
     1.6  
     1.7 -val HOL_ss = empty_ss
     1.8 +val HOL_base_ss = empty_ss
     1.9        setmksimps (mksimps mksimps_pairs)
    1.10 -      setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac
    1.11 -                             ORELSE' etac FalseE)
    1.12 -      setsubgoaler asm_simp_tac
    1.13 +      setsubgoaler asm_simp_tac;
    1.14 +
    1.15 +val HOL_min_ss = HOL_base_ss setsolver (fn ps => 
    1.16 +	FIRST'[resolve_tac (TrueI::refl::ps), atac, etac FalseE]);
    1.17 +
    1.18 +val HOL_safe_min_ss = HOL_base_ss setsolver (fn ps => 
    1.19 +	FIRST'[match_tac (TrueI::refl::ps), eq_assume_tac, ematch_tac[FalseE]]);
    1.20 +
    1.21 +val HOL_ss = HOL_min_ss
    1.22        addsimps ([if_True, if_False, if_cancel,
    1.23  		 o_apply, imp_disjL, conj_assoc, disj_assoc,
    1.24                   de_Morgan_conj, de_Morgan_disj, not_all, not_ex, cases_simp]