--- 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