# HG changeset patch
# User paulson
# Date 843566067 -7200
# Node ID 9d47e2962edda979a4c8b406ee5747eade94f031
# Parent  dd5866263153951a8b5502f4c5fb77702296fd78
Fixed spelling error in comment

diff -r dd5866263153 -r 9d47e2962edd src/HOL/simpdata.ML
--- a/src/HOL/simpdata.ML	Tue Sep 24 13:53:18 1996 +0200
+++ b/src/HOL/simpdata.ML	Tue Sep 24 13:54:27 1996 +0200
@@ -228,7 +228,7 @@
 end;
 
 
-(* eliminiation of existential quantifiers in assumptions *)
+(* elimination of existential quantifiers in assumptions *)
 
 val ex_all_equiv =
   let val lemma1 = prove_goal HOL.thy
@@ -242,13 +242,25 @@
 (* '&' congruence rule: not included by default!
    May slow rewrite proofs down by as much as 50% *)
 
-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);
+val conj_cong = 
+  let val th = prove_goal HOL.thy 
+                "(P=P')--> (P'--> (Q=Q'))--> ((P&Q) = (P'&Q'))"
+		(fn _=> [fast_tac HOL_cs 1])
+  in  standard (impI RSN (2, th RS mp RS mp))  end;
 
-val rev_conj_cong = impI RSN
-    (2, prove_goal HOL.thy "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))"
-        (fn _=> [fast_tac HOL_cs 1]) RS mp RS mp);
+val rev_conj_cong =
+  let val th = prove_goal HOL.thy 
+                "(Q=Q')--> (Q'--> (P=P'))--> ((P&Q) = (P'&Q'))"
+		(fn _=> [fast_tac HOL_cs 1])
+  in  standard (impI RSN (2, th RS mp RS mp))  end;
+
+(* '|' congruence rule: not included by default! *)
+
+val disj_cong = 
+  let val th = prove_goal HOL.thy 
+                "(P=P')--> (~P'--> (Q=Q'))--> ((P|Q) = (P'|Q'))"
+		(fn _=> [fast_tac HOL_cs 1])
+  in  standard (impI RSN (2, th RS mp RS mp))  end;
 
 (** 'if' congruence rules: neither included by default! *)