--- 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;
*}
(*>*)
--- 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]
+}
--- 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*)
--- 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*)
--- 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*)
--- 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*)
--- 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*)