src/Pure/drule.ML
changeset 12297 2ce7b42b0a64
parent 12283 d42aa776889e
child 12373 704e50ab65af
--- 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