--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Tue Jun 05 15:16:10 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML Tue Jun 05 15:16:11 2007 +0200
@@ -1,6 +1,14 @@
structure ROOT =
struct
+structure HOL =
+struct
+
+type 'a eq = {eq : 'a -> 'a -> bool};
+fun eq (A_:'a eq) = #eq A_;
+
+end; (*struct HOL*)
+
structure Orderings =
struct
@@ -10,20 +18,12 @@
end; (*struct Orderings*)
-structure Code_Generator =
-struct
-
-type 'a eq = {eq : 'a -> 'a -> bool};
-fun eq (A_:'a eq) = #eq A_;
-
-end; (*struct Code_Generator*)
-
structure Codegen =
struct
fun less_eq_product (A1_, A2_) B_ (x1, y1) (x2, y2) =
Orderings.less A2_ x1 x2 orelse
- Code_Generator.eq A1_ x1 x2 andalso Orderings.less_eq B_ y1 y2;
+ HOL.eq A1_ x1 x2 andalso Orderings.less_eq B_ y1 y2;
end; (*struct Codegen*)