added remdups_rl;
authorwenzelm
Mon Nov 26 18:33:21 2001 +0100 (2001-11-26)
changeset 122972ce7b42b0a64
parent 12296 45269a593e1b
child 12298 b344486c33e2
added remdups_rl;
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Mon Nov 26 18:33:08 2001 +0100
     1.2 +++ b/src/Pure/drule.ML	Mon Nov 26 18:33:21 2001 +0100
     1.3 @@ -121,6 +121,7 @@
     1.4    val unvarifyT: thm -> thm
     1.5    val unvarify: thm -> thm
     1.6    val tvars_intr_list: string list -> thm -> thm
     1.7 +  val remdups_rl: thm
     1.8    val conj_intr: thm -> thm -> thm
     1.9    val conj_intr_list: thm list -> thm
    1.10    val conj_elim: thm -> thm * thm
    1.11 @@ -643,9 +644,15 @@
    1.12    end;
    1.13  
    1.14  
    1.15 +(* "[| PROP ?phi; PROP ?phi; PROP ?psi |] ==> PROP ?psi" *)
    1.16 +
    1.17 +val remdups_rl =
    1.18 +  let val P = read_prop "PROP phi" and Q = read_prop "PROP psi";
    1.19 +  in store_standard_thm_open "remdups_rl" (implies_intr_list [P, P, Q] (Thm.assume Q)) end;
    1.20 +
    1.21 +
    1.22  (*(PROP ?phi ==> (!!x. PROP ?psi(x))) == (!!x. PROP ?phi ==> PROP ?psi(x))
    1.23 -  Rewrite rule for HHF normalization.
    1.24 -*)
    1.25 +  Rewrite rule for HHF normalization.*)
    1.26  
    1.27  val norm_hhf_eq =
    1.28    let