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.
code generator setup for "int" also works under eta-contraction
authorhaftmann
Mon, 30 Jun 2008 13:41:28 +0200
changeset 27395 67330748a72e
parent 27394 facb528f1834
child 27396 77ea650bfc3a
code generator setup for "int" also works under eta-contraction
src/HOL/Int.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Int.thy	Sat Jun 28 23:52:43 2008 +0200
+++ b/src/HOL/Int.thy	Mon Jun 30 13:41:28 2008 +0200
@@ -1924,7 +1924,7 @@
 lemmas int_aux_code = of_nat_aux_code [where ?'a = int, simplified int_aux_def [symmetric], code]
 
 lemma [code, code unfold, code inline del]:
-  "of_nat n = int_aux n 0"
+  "of_nat = (\<lambda>n. int_aux n 0)"
   by (simp add: int_aux_def of_nat_aux_def)
 
 definition
isabelle