--- 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*)