--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML Fri Mar 02 15:43:16 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML Fri Mar 02 15:43:17 2007 +0100
@@ -8,6 +8,17 @@
end; (*struct Nat*)
+structure Integer =
+struct
+
+fun nat_aux n i =
+ (if IntInf.<= (i, (0 : IntInf.int)) then n
+ else nat_aux (Nat.Suc n) (IntInf.- (i, (1 : IntInf.int))));
+
+fun nat i = nat_aux Nat.Zero_nat i;
+
+end; (*struct Integer*)
+
structure Codegen =
struct
@@ -15,7 +26,7 @@
val foobar_set : Nat.nat list =
Nat.Zero_nat ::
- (Nat.Suc Nat.Zero_nat :: (Nat.Suc (Nat.Suc Nat.Zero_nat) :: []));
+ (Nat.Suc Nat.Zero_nat :: (Integer.nat (2 : IntInf.int) :: []));
end; (*struct Codegen*)