src/Pure/conv.ML
changeset 23490 1dfbfc92017a
parent 23411 c524900454f3
child 23534 3f82d1798976
     1.1 --- a/src/Pure/conv.ML	Mon Jun 25 00:36:38 2007 +0200
     1.2 +++ b/src/Pure/conv.ML	Mon Jun 25 00:36:39 2007 +0200
     1.3 @@ -8,11 +8,13 @@
     1.4  infix 1 then_conv;
     1.5  infix 0 else_conv;
     1.6  
     1.7 +type conv = cterm -> thm;
     1.8 +
     1.9  signature CONV =
    1.10  sig
    1.11 -  type conv = cterm -> thm
    1.12    val no_conv: conv
    1.13    val all_conv: conv
    1.14 +  val is_refl: thm -> bool
    1.15    val then_conv: conv * conv -> conv
    1.16    val else_conv: conv * conv -> conv
    1.17    val first_conv: conv list -> conv
    1.18 @@ -32,9 +34,7 @@
    1.19    val concl_conv: int -> conv -> conv
    1.20    val prems_conv: int -> (int -> conv) -> conv
    1.21    val goals_conv: (int -> bool) -> conv -> conv
    1.22 -  val eta_conv: theory -> conv 
    1.23    val fconv_rule: conv -> thm -> thm
    1.24 -  val is_refl: thm -> bool
    1.25  end;
    1.26  
    1.27  structure Conv: CONV =
    1.28 @@ -143,11 +143,6 @@
    1.29  
    1.30  fun goals_conv pred cv = prems_conv ~1 (fn i => if pred i then cv else all_conv);
    1.31  
    1.32 -fun eta_conv thy ct = 
    1.33 -  let val {t, ...} = rep_cterm ct
    1.34 -      val ct' = cterm_of thy (Pattern.eta_long [] t)
    1.35 -  in (symmetric o eta_conversion) ct'
    1.36 -  end;
    1.37 +fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
    1.38  
    1.39 -fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
    1.40  end;