doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
changeset 21189 5435ccdb4ea1
parent 21147 737a94f047e3
child 21993 4b802a9e0738
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Mon Nov 06 12:04:44 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Mon Nov 06 16:28:29 2006 +0100
@@ -1,5 +1,5 @@
 module Codegen where
-import qualified IntDef
+import qualified Nat
 
 class Null a where
   null :: a
@@ -14,5 +14,5 @@
 instance Codegen.Null (Maybe b) where
   null = Codegen.null_option
 
-dummy :: Maybe IntDef.Nat
-dummy = Codegen.head [Just (IntDef.Succ_nat IntDef.Zero_nat), Nothing]
+dummy :: Maybe Nat.Nat
+dummy = Codegen.head [Just (Nat.Suc Nat.Zero_nat), Nothing]