--- 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*)