# HG changeset patch
# User wenzelm
# Date 1006796001 -3600
# Node ID 2ce7b42b0a64c19b994ba1247a08750ba020a26e
# Parent  45269a593e1b82cc69b52828594d5920ee1626a7
added remdups_rl;

diff -r 45269a593e1b -r 2ce7b42b0a64 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon Nov 26 18:33:08 2001 +0100
+++ b/src/Pure/drule.ML	Mon Nov 26 18:33:21 2001 +0100
@@ -121,6 +121,7 @@
   val unvarifyT: thm -> thm
   val unvarify: thm -> thm
   val tvars_intr_list: string list -> thm -> thm
+  val remdups_rl: thm
   val conj_intr: thm -> thm -> thm
   val conj_intr_list: thm list -> thm
   val conj_elim: thm -> thm * thm
@@ -643,9 +644,15 @@
   end;
 
 
+(* "[| PROP ?phi; PROP ?phi; PROP ?psi |] ==> PROP ?psi" *)
+
+val remdups_rl =
+  let val P = read_prop "PROP phi" and Q = read_prop "PROP psi";
+  in store_standard_thm_open "remdups_rl" (implies_intr_list [P, P, Q] (Thm.assume Q)) end;
+
+
 (*(PROP ?phi ==> (!!x. PROP ?psi(x))) == (!!x. PROP ?phi ==> PROP ?psi(x))
-  Rewrite rule for HHF normalization.
-*)
+  Rewrite rule for HHF normalization.*)
 
 val norm_hhf_eq =
   let