# HG changeset patch
# User berghofe
# Date 1004554835 -3600
# Node ID bc9b5bad0e7bc451c0666764249c1be23f4ccba4
# Parent  81be0a855397f4a2f3648f109cfbab254e5a729b
Additional rules for simplifying inside "Goal"

diff -r 81be0a855397 -r bc9b5bad0e7b src/Pure/Proof/proof_rewrite_rules.ML
--- a/src/Pure/Proof/proof_rewrite_rules.ML	Wed Oct 31 19:59:21 2001 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Wed Oct 31 20:00:35 2001 +0100
@@ -25,6 +25,20 @@
       (PAxm ("ProtoPure.equal_intr", _, _) % A % B %% prf1 %% prf2)) =
           Some (equal_intr_axm % B % A %% prf2 %% prf1)
 
+  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %%
+      (PAxm ("ProtoPure.combination", _, _) % Some (Const ("Goal", _)) %
+        _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %%
+      ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
+      Some (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
+
+  | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some (_ $ A) % Some (_ $ B) %%
+      (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
+        (PAxm ("ProtoPure.combination", _, _) % Some (Const ("Goal", _)) %
+           _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %%
+      ((tg as PThm (("ProtoPure.triv_goal", _), _, _, _)) % _ %% prf2)) =
+      Some (tg %> B %% (equal_elim_axm %> A %> B %%
+        (symmetric_axm % None % None %% prf1) %% prf2))
+
   | rew _ (PAxm ("ProtoPure.equal_elim", _, _) % Some X % Some Y %%
       (PAxm ("ProtoPure.combination", _, _) % _ % _ % _ % _ %%
         (PAxm ("ProtoPure.combination", _, _) % Some (Const ("==>", _)) % _ % _ % _ %%