# HG changeset patch
# User nipkow
# Date 757795145 -3600
# Node ID 2fdeeae553acf1fa202d871d21a079cfbe4572ea
# Parent  9769afcc1c4ec408ba13c5e8e9539b05ecca3d13
modified solver of HOL_ss to take the new simplifier into account: the thm to
be solved may have assumption.

diff -r 9769afcc1c4e -r 2fdeeae553ac simpdata.ML
--- a/simpdata.ML	Wed Jan 05 19:37:07 1994 +0100
+++ b/simpdata.ML	Wed Jan 05 19:39:05 1994 +0100
@@ -59,7 +59,7 @@
    "(P & False) = False", "(False & P) = False", "(P & P) = P",
    "(P | True) = True", "(True | P) = True", 
    "(P | False) = P", "(False | P) = P", "(P | P) = P",
-   "(!x.P) = P",
+   "(!x.P) = P", "(? x.P) = P",
    "(P|Q --> R) = ((P-->R)&(Q-->R))" ];
 
 val meta_obj_reflection = prove_goal HOL.thy "x==y ==> x=y"
@@ -92,7 +92,7 @@
 
 val HOL_ss = empty_ss
       setmksimps mk_rews
-      setsolver (fn prems => resolve_tac (TrueI::refl::prems))
+      setsolver (fn prems => resolve_tac (TrueI::refl::prems) ORELSE' atac)
       setsubgoaler asm_simp_tac
       addsimps ([if_True, if_False, o_apply] @ simp_thms)
       addcongs [imp_cong];
@@ -100,6 +100,12 @@
 fun split_tac splits =
   mk_case_split_tac (meta_obj_reflection RS iffD2) (map mk_eq splits);
 
+(** '&' congruence rule: not included by default! *)
+
+val conj_cong = impI RSN
+    (2, prove_goal HOL.thy "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
+	(fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
+
 (** 'if' congruence rules: neither included by default! *)
 
 (*Simplifies x assuming c and y assuming ~c*)