src/Pure/drule.ML
changeset 20227 435601e8e53d
parent 20077 4fc9a4fef219
child 20260 990dbc007ca6
     1.1 --- a/src/Pure/drule.ML	Thu Jul 27 13:43:04 2006 +0200
     1.2 +++ b/src/Pure/drule.ML	Thu Jul 27 13:43:05 2006 +0200
     1.3 @@ -67,8 +67,6 @@
     1.4    val equals_cong: thm
     1.5    val imp_cong: thm
     1.6    val swap_prems_eq: thm
     1.7 -  val equal_abs_elim: cterm  -> thm -> thm
     1.8 -  val equal_abs_elim_list: cterm list -> thm -> thm
     1.9    val asm_rl: thm
    1.10    val cut_rl: thm
    1.11    val revcut_rl: thm
    1.12 @@ -914,24 +912,6 @@
    1.13  end;
    1.14  
    1.15  
    1.16 -(** Derived rules mainly for METAHYPS **)
    1.17 -
    1.18 -(*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*)
    1.19 -fun equal_abs_elim ca eqth =
    1.20 -  let val {thy=thya, t=a, ...} = rep_cterm ca
    1.21 -      and combth = combination eqth (reflexive ca)
    1.22 -      val {thy,prop,...} = rep_thm eqth
    1.23 -      val (abst,absu) = Logic.dest_equals prop
    1.24 -      val cert = cterm_of (Theory.merge (thy,thya))
    1.25 -  in  transitive (symmetric (beta_conversion false (cert (abst$a))))
    1.26 -           (transitive combth (beta_conversion false (cert (absu$a))))
    1.27 -  end
    1.28 -  handle THM _ => raise THM("equal_abs_elim", 0, [eqth]);
    1.29 -
    1.30 -(*Calling equal_abs_elim with multiple terms*)
    1.31 -fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) th (rev cts);
    1.32 -
    1.33 -
    1.34  (* global schematic variables *)
    1.35  
    1.36  fun unvarify th =