--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Fri Jan 05 14:30:08 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs Fri Jan 05 14:31:44 2007 +0100
@@ -1,18 +1,23 @@
-module Codegen where
-import qualified Nat
+module Codegen where {
+
+import qualified Nat;
-class Null a where
- nulla :: a
+class Null a where {
+ nulla :: a;
+};
+
+heada :: (Codegen.Null a) => [a] -> a;
+heada (y : xs) = y;
+heada [] = Codegen.nulla;
-heada :: (Codegen.Null a) => ([a] -> a)
-heada (y : xs) = y
-heada [] = Codegen.nulla
+null_option :: Maybe b;
+null_option = Nothing;
-null_option :: Maybe b
-null_option = Nothing
+instance Codegen.Null (Maybe b) where {
+ nulla = Codegen.null_option;
+};
-instance Codegen.Null (Maybe b) where
- null = Codegen.null_option
+dummy :: Maybe Nat.Nat;
+dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing];
-dummy :: Maybe Nat.Nat
-dummy = Codegen.heada [Just (Nat.Suc Nat.Zero_nat), Nothing]
+}