src/Pure/drule.ML
changeset 13325 5b5e12f0aee0
parent 13198 3e40f48a500f
child 13368 8f8ba32d148b
     1.1 --- a/src/Pure/drule.ML	Tue Jul 09 17:25:42 2002 +0200
     1.2 +++ b/src/Pure/drule.ML	Tue Jul 09 18:03:26 2002 +0200
     1.3 @@ -130,6 +130,7 @@
     1.4    val conj_elim_list: thm -> thm list
     1.5    val conj_elim_precise: int -> thm -> thm list
     1.6    val conj_intr_thm: thm
     1.7 +  val abs_def: thm -> thm
     1.8  end;
     1.9  
    1.10  structure Drule: DRULE =
    1.11 @@ -589,6 +590,16 @@
    1.12  
    1.13  val refl_implies = reflexive implies;
    1.14  
    1.15 +fun abs_def thm =
    1.16 +  let
    1.17 +    val (_, cvs) = strip_comb (fst (dest_equals (cprop_of thm)));
    1.18 +    val thm' = foldr (fn (ct, thm) => Thm.abstract_rule
    1.19 +      (case term_of ct of Var ((a, _), _) => a | Free (a, _) => a | _ => "x")
    1.20 +        ct thm) (cvs, thm)
    1.21 +  in transitive
    1.22 +    (symmetric (eta_conversion (fst (dest_equals (cprop_of thm'))))) thm'
    1.23 +  end;
    1.24 +
    1.25  
    1.26  (*** Some useful meta-theorems ***)
    1.27