# HG changeset patch
# User oheimb
# Date 850918354 -3600
# Node ID a81d4c219c3c434380e7aa8cde44bb23a5b057d7
# Parent  6663e0d210b0d0cd179e37c1a453001336828d1e
factored out HOL_base_ss and val HOL_min_ss, added HOL_safe_min_ss

diff -r 6663e0d210b0 -r a81d4c219c3c src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Wed Dec 18 15:11:07 1996 +0100
+++ b/src/HOL/simpdata.ML	Wed Dec 18 15:12:34 1996 +0100
@@ -307,11 +307,17 @@
    ("All", [spec]), ("True", []), ("False", []),
    ("If", [if_bool_eq RS iffD1])];
 
-val HOL_ss = empty_ss
+val HOL_base_ss = empty_ss
       setmksimps (mksimps mksimps_pairs)
-      setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac
-                             ORELSE' etac FalseE)
-      setsubgoaler asm_simp_tac
+      setsubgoaler asm_simp_tac;
+
+val HOL_min_ss = HOL_base_ss setsolver (fn ps => 
+	FIRST'[resolve_tac (TrueI::refl::ps), atac, etac FalseE]);
+
+val HOL_safe_min_ss = HOL_base_ss setsolver (fn ps => 
+	FIRST'[match_tac (TrueI::refl::ps), eq_assume_tac, ematch_tac[FalseE]]);
+
+val HOL_ss = HOL_min_ss
       addsimps ([if_True, if_False, if_cancel,
 		 o_apply, imp_disjL, conj_assoc, disj_assoc,
                  de_Morgan_conj, de_Morgan_disj, not_all, not_ex, cases_simp]