Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
export beta_eta_conversion;
authorwenzelm
Wed, 16 Jan 2002 20:58:27 +0100
changeset 12779 c5739c1431ab
parent 12778 3120e338ffae
child 12780 6b41c750451c
export beta_eta_conversion;
src/Pure/meta_simplifier.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/meta_simplifier.ML	Wed Jan 16 20:57:02 2002 +0100
+++ b/src/Pure/meta_simplifier.ML	Wed Jan 16 20:58:27 2002 +0100
@@ -39,6 +39,7 @@
   val set_mk_sym        : meta_simpset * (thm -> thm option) -> meta_simpset
   val set_mk_eq_True    : meta_simpset * (thm -> thm option) -> meta_simpset
   val set_termless      : meta_simpset * (term * term -> bool) -> meta_simpset
+  val beta_eta_conversion: cterm -> thm
   val rewrite_cterm: bool * bool * bool ->
     (meta_simpset -> thm -> thm option) -> meta_simpset -> cterm -> thm
   val goals_conv        : (int -> bool) -> (cterm -> thm) -> cterm -> thm
isabelle