# HG changeset patch
# User wenzelm
# Date 1026837423 -7200
# Node ID 8f8ba32d148be1a183b57d8bfe04bc29dab375b1
# Parent  ad307f0d80db39dca51616f4dcadef3a446619b7
added equal_elim_rule1;

diff -r ad307f0d80db -r 8f8ba32d148b src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Jul 16 18:26:52 2002 +0200
+++ b/src/Pure/drule.ML	Tue Jul 16 18:37:03 2002 +0200
@@ -77,6 +77,7 @@
   val triv_forall_equality: thm
   val swap_prems_rl     : thm
   val equal_intr_rule   : thm
+  val equal_elim_rule1  : thm
   val inst              : string -> string -> thm -> thm
   val instantiate'      : ctyp option list -> cterm option list -> thm -> thm
   val incr_indexes_wrt  : int list -> ctyp list -> cterm list -> thm list -> thm -> thm
@@ -667,6 +668,13 @@
       (implies_intr PQ (implies_intr QP (equal_intr (assume PQ) (assume QP))))
   end;
 
+(* [| PROP ?phi == PROP ?psi; PROP ?phi |] ==> PROP ?psi *)
+val equal_elim_rule1 =
+  let val eq = read_prop "PROP phi == PROP psi"
+      and P = read_prop "PROP phi"
+  in store_standard_thm_open "equal_elim_rule1"
+    (Thm.equal_elim (assume eq) (assume P) |> implies_intr_list [eq, P])
+  end;
 
 (* "[| PROP ?phi; PROP ?phi; PROP ?psi |] ==> PROP ?psi" *)