src/Pure/conv.ML
changeset 23411 c524900454f3
parent 23169 37091da05d8e
child 23490 1dfbfc92017a
     1.1 --- a/src/Pure/conv.ML	Sun Jun 17 13:39:45 2007 +0200
     1.2 +++ b/src/Pure/conv.ML	Sun Jun 17 13:39:48 2007 +0200
     1.3 @@ -32,7 +32,9 @@
     1.4    val concl_conv: int -> conv -> conv
     1.5    val prems_conv: int -> (int -> conv) -> conv
     1.6    val goals_conv: (int -> bool) -> conv -> conv
     1.7 +  val eta_conv: theory -> conv 
     1.8    val fconv_rule: conv -> thm -> thm
     1.9 +  val is_refl: thm -> bool
    1.10  end;
    1.11  
    1.12  structure Conv: CONV =
    1.13 @@ -140,6 +142,12 @@
    1.14    in conv 1 end;
    1.15  
    1.16  fun goals_conv pred cv = prems_conv ~1 (fn i => if pred i then cv else all_conv);
    1.17 -fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
    1.18  
    1.19 +fun eta_conv thy ct = 
    1.20 +  let val {t, ...} = rep_cterm ct
    1.21 +      val ct' = cterm_of thy (Pattern.eta_long [] t)
    1.22 +  in (symmetric o eta_conversion) ct'
    1.23 +  end;
    1.24 +
    1.25 +fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
    1.26  end;