--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Thu Jan 04 15:29:44 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Thu Jan 04 17:11:09 2007 +0100
@@ -2,11 +2,10 @@
import qualified Nat
class Null a where
- null :: a
+ nulla :: a
-head :: (Codegen.Null a_1) => [a_1] -> a_1
-head (y : xs) = y
-head [] = Codegen.null
+heada :: (Codegen.Null a) => ([a] -> a)
+heada (y : xs) = y
null_option :: Maybe b
null_option = Nothing
@@ -15,4 +14,4 @@
null = Codegen.null_option
dummy :: Maybe Nat.Nat
-dummy = Codegen.head [Just (Nat.Suc Nat.Zero_nat), Nothing]
+dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing]