# HG changeset patch
# User chaieb
# Date 1182080388 -7200
# Node ID c524900454f367774a6361edd03000af26dcca71
# Parent  f44d7233a54b007e2ad5c9a9c1e5dd232ff5aa0d
Added eta_conv and eta-expansion conversion: waiting for it to be in thm.ML; exported is_refl

diff -r f44d7233a54b -r c524900454f3 src/Pure/conv.ML
--- a/src/Pure/conv.ML	Sun Jun 17 13:39:45 2007 +0200
+++ b/src/Pure/conv.ML	Sun Jun 17 13:39:48 2007 +0200
@@ -32,7 +32,9 @@
   val concl_conv: int -> conv -> conv
   val prems_conv: int -> (int -> conv) -> conv
   val goals_conv: (int -> bool) -> conv -> conv
+  val eta_conv: theory -> conv 
   val fconv_rule: conv -> thm -> thm
+  val is_refl: thm -> bool
 end;
 
 structure Conv: CONV =
@@ -140,6 +142,12 @@
   in conv 1 end;
 
 fun goals_conv pred cv = prems_conv ~1 (fn i => if pred i then cv else all_conv);
-fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
 
+fun eta_conv thy ct = 
+  let val {t, ...} = rep_cterm ct
+      val ct' = cterm_of thy (Pattern.eta_long [] t)
+  in (symmetric o eta_conversion) ct'
+  end;
+
+fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
 end;