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.
beta/eta conversion after preprocessor
authorhaftmann
Thu, 10 May 2007 22:11:36 +0200
changeset 22928 1feef3b54ce1
parent 22927 0b53bd36258b
child 22929 e6b6f8dd03e9
beta/eta conversion after preprocessor
src/HOL/Library/EfficientNat.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/EfficientNat.thy	Thu May 10 22:11:35 2007 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Thu May 10 22:11:36 2007 +0200
@@ -366,7 +366,8 @@
 fun lift_obj_eq f thy =
   map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
   #> f thy
-  #> map (fn thm => thm RS @{thm eq_reflection});
+  #> map (fn thm => thm RS @{thm eq_reflection})
+  #> map (Conv.fconv_rule Drule.beta_eta_conversion)
 *}
 
 setup {*
isabelle