doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
changeset 21189 5435ccdb4ea1
parent 21147 737a94f047e3
child 21993 4b802a9e0738
     1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Mon Nov 06 12:04:44 2006 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs	Mon Nov 06 16:28:29 2006 +0100
     1.3 @@ -1,5 +1,5 @@
     1.4  module Codegen where
     1.5 -import qualified IntDef
     1.6 +import qualified Nat
     1.7  
     1.8  class Null a where
     1.9    null :: a
    1.10 @@ -14,5 +14,5 @@
    1.11  instance Codegen.Null (Maybe b) where
    1.12    null = Codegen.null_option
    1.13  
    1.14 -dummy :: Maybe IntDef.Nat
    1.15 -dummy = Codegen.head [Just (IntDef.Succ_nat IntDef.Zero_nat), Nothing]
    1.16 +dummy :: Maybe Nat.Nat
    1.17 +dummy = Codegen.head [Just (Nat.Suc Nat.Zero_nat), Nothing]