# HG changeset patch
# User wenzelm
# Date 1140643121 -3600
# Node ID a3cf88213ea54064c79f2d8f676298951f2ccf5c
# Parent  59b26248547b80cb46bc66cf5e3dab32731eba35
rew: handle conjunctionI/D1/D2;

diff -r 59b26248547b -r a3cf88213ea5 src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Wed Feb 22 22:18:39 2006 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Wed Feb 22 22:18:41 2006 +0100
@@ -34,6 +34,10 @@
 
     fun rew' _ (PThm (("ProtoPure.protectD", _), _, _, _) % _ %%
         (PThm (("ProtoPure.protectI", _), _, _, _) % _ %% prf)) = SOME prf
+      | rew' _ (PThm (("ProtoPure.conjunctionD1", _), _, _, _) % _ % _ %%
+        (PThm (("ProtoPure.conjunctionI", _), _, _, _) % _ % _ %% prf %% _)) = SOME prf
+      | rew' _ (PThm (("ProtoPure.conjunctionD2", _), _, _, _) % _ % _ %%
+        (PThm (("ProtoPure.conjunctionI", _), _, _, _) % _ % _ %% _ %% prf)) = SOME prf
       | rew' _ (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
         (PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
       | rew' _ (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%