# HG changeset patch
# User haftmann
# Date 1168003904 -3600
# Node ID 12b94d7f7e1fd9aedbaddae708620fb2eb22e4a8
# Parent  4b70cbd9600703a96b577cbcff5e09ff8323d873
adaptions

diff -r 4b70cbd96007 -r 12b94d7f7e1f doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Jan 05 14:30:08 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Fri Jan 05 14:31:44 2007 +0100
@@ -8,7 +8,7 @@
 begin
 
 ML {*
-CodegenSerializer.sml_code_width := 74;
+CodegenSerializer.code_width := 74;
 *}
 
 (*>*)
diff -r 4b70cbd96007 -r 12b94d7f7e1f doc-src/IsarAdvanced/Codegen/Thy/examples/Codegen.hs
--- 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]
+}
diff -r 4b70cbd96007 -r 12b94d7f7e1f doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML	Fri Jan 05 14:30:08 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/bool_infix.ML	Fri Jan 05 14:31:44 2007 +0100
@@ -26,7 +26,7 @@
 struct
 
 fun in_interval (k, l) n =
-  (Nat.less_eq_nat k n andalso Nat.less_eq_nat n l);
+  Nat.less_eq_nat k n andalso Nat.less_eq_nat n l;
 
 end; (*struct Codegen*)
 
diff -r 4b70cbd96007 -r 12b94d7f7e1f doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Fri Jan 05 14:30:08 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Fri Jan 05 14:31:44 2007 +0100
@@ -13,7 +13,7 @@
 struct
 
 fun memberl (A_:'a Code_Generator.eq) x (y :: ys) =
-  (Code_Generator.op_eq A_ x y orelse memberl A_ x ys)
+  Code_Generator.op_eq A_ x y orelse memberl A_ x ys
   | memberl (A_:'a Code_Generator.eq) x [] = false;
 
 end; (*struct List*)
diff -r 4b70cbd96007 -r 12b94d7f7e1f doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML	Fri Jan 05 14:30:08 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/dirty_set.ML	Fri Jan 05 14:31:44 2007 +0100
@@ -11,11 +11,11 @@
 structure Codegen = 
 struct
 
-val dummy_set : (Nat.nat -> Nat.nat) list = (Nat.Suc :: []);
+val dummy_set : (Nat.nat -> Nat.nat) list = Nat.Suc :: [];
 
 val foobar_set : Nat.nat list =
-  (Nat.Zero_nat ::
-    (Nat.Suc Nat.Zero_nat :: (Nat.Suc (Nat.Suc Nat.Zero_nat) :: [])));
+  Nat.Zero_nat ::
+    (Nat.Suc Nat.Zero_nat :: (Nat.Suc (Nat.Suc Nat.Zero_nat) :: []));
 
 end; (*struct Codegen*)
 
diff -r 4b70cbd96007 -r 12b94d7f7e1f doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML	Fri Jan 05 14:30:08 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/integers.ML	Fri Jan 05 14:31:44 2007 +0100
@@ -4,8 +4,8 @@
 structure Codegen = 
 struct
 
-val double_inc : IntInf.int -> IntInf.int =
-  (fn k => IntInf.+ ((IntInf.* ((2 : IntInf.int), k)), (1 : IntInf.int)));
+fun double_inc k =
+  IntInf.+ ((IntInf.* ((2 : IntInf.int), k)), (1 : IntInf.int));
 
 end; (*struct Codegen*)
 
diff -r 4b70cbd96007 -r 12b94d7f7e1f doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML	Fri Jan 05 14:30:08 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML	Fri Jan 05 14:31:44 2007 +0100
@@ -12,9 +12,9 @@
 structure Product_Type = 
 struct
 
-fun op_eq_prod (A_:'a Code_Generator.eq) (B_:'b Code_Generator.eq) (x1, y1)
-  (x2, y2) =
-  (Code_Generator.op_eq A_ x1 x2 andalso Code_Generator.op_eq B_ y1 y2);
+fun op_eq_prod (A_:'a Code_Generator.eq) (B_:'b Code_Generator.eq)
+  (x1, y1) (x2, y2) =
+  Code_Generator.op_eq A_ x1 x2 andalso Code_Generator.op_eq B_ y1 y2;
 
 end; (*struct Product_Type*)
 
@@ -36,15 +36,15 @@
     val (x1, y1) = p1;
     val (x2, y2) = p2;
   in
-    (Orderings.less (#2 B_) x1 x2 orelse
+    Orderings.less (#2 B_) x1 x2 orelse
       Code_Generator.op_eq (#1 B_) x1 x2 andalso
-        Orderings.less (#2 C_) y1 y2)
+        Orderings.less (#2 C_) y1 y2
   end;
 
 fun less_eq_prod (B_:'b Code_Generator.eq * 'b Orderings.ord)
   (C_:'c Code_Generator.eq * 'c Orderings.ord) p1 p2 =
-  (less_prod ((#1 B_), (#2 B_)) ((#1 C_), (#2 C_)) p1 p2 orelse
-    Product_Type.op_eq_prod (#1 B_) (#1 C_) p1 p2);
+  less_prod ((#1 B_), (#2 B_)) ((#1 C_), (#2 C_)) p1 p2 orelse
+    Product_Type.op_eq_prod (#1 B_) (#1 C_) p1 p2;
 
 end; (*struct Codegen*)