Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
rew: handle conjunctionI/D1/D2;
authorwenzelm
Wed, 22 Feb 2006 22:18:41 +0100
changeset 19126 a3cf88213ea5
parent 19125 59b26248547b
child 19127 9aff3d859d39
rew: handle conjunctionI/D1/D2;
src/Pure/Proof/proof_rewrite_rules.ML file | annotate | diff | comparison | revisions 
--- 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", _, _) % _ % _ %%
isabelle