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.
Locally added definition of "int :: nat => int" again to make
authorberghofe
Fri, 15 Jun 2007 19:19:23 +0200
changeset 23399 1766da98eaa9
parent 23398 0b5a400c7595
child 23400 a64b39e5809b
Locally added definition of "int :: nat => int" again to make code generation work.
src/HOL/Lambda/WeakNorm.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Lambda/WeakNorm.thy	Fri Jun 15 15:10:32 2007 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Fri Jun 15 19:19:23 2007 +0200
@@ -575,6 +575,10 @@
   CodegenSerializer.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
 *}
 
+definition
+  int :: "nat \<Rightarrow> int" where
+  "int \<equiv> of_nat"
+
 code_gen type_NF nat int in SML
 
 ML {*
@@ -584,7 +588,7 @@
 structure Nat = ROOT.Nat;
 
 val nat_of_int = ROOT.Integer.nat o IntInf.fromInt;
-val int_of_nat = IntInf.toInt o ROOT.Integer.int;
+val int_of_nat = IntInf.toInt o ROOT.WeakNorm.int;
 
 fun dBtype_of_typ (Type ("fun", [T, U])) =
       Type.Fun (dBtype_of_typ T, dBtype_of_typ U)
isabelle