# HG changeset patch
# User haftmann
# Date 1181049371 -7200
# Node ID 9886802cbbd67dd0d8eb2c89d0929b63d72e1c82
# Parent  9ef65be6bb2a7206e68464b52b2d97b54c31386a
updated documentation

diff -r 9ef65be6bb2a -r 9886802cbbd6 doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Tue Jun 05 15:16:10 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Tue Jun 05 15:16:11 2007 +0200
@@ -1,19 +1,18 @@
 structure ROOT = 
 struct
 
-structure Code_Generator = 
+structure HOL = 
 struct
 
 type 'a eq = {eq : 'a -> 'a -> bool};
 fun eq (A_:'a eq) = #eq A_;
 
-end; (*struct Code_Generator*)
+end; (*struct HOL*)
 
 structure List = 
 struct
 
-fun memberl A_ x (y :: ys) =
-  Code_Generator.eq A_ x y orelse memberl A_ x ys
+fun memberl A_ x (y :: ys) = HOL.eq A_ x y orelse memberl A_ x ys
   | memberl A_ x [] = false;
 
 end; (*struct List*)
diff -r 9ef65be6bb2a -r 9886802cbbd6 doc-src/IsarAdvanced/Codegen/Thy/examples/lexicographic.ML
--- 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*)
 
diff -r 9ef65be6bb2a -r 9886802cbbd6 doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML	Tue Jun 05 15:16:10 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/set_list.ML	Tue Jun 05 15:16:11 2007 +0200
@@ -1,13 +1,13 @@
 structure ROOT = 
 struct
 
-structure Code_Generator = 
+structure HOL = 
 struct
 
 type 'a eq = {eq : 'a -> 'a -> bool};
 fun eq (A_:'a eq) = #eq A_;
 
-end; (*struct Code_Generator*)
+end; (*struct HOL*)
 
 structure List = 
 struct
@@ -15,8 +15,7 @@
 fun foldr f (x :: xs) a = f x (foldr f xs a)
   | foldr f [] a = a;
 
-fun memberl A_ x (y :: ys) =
-  Code_Generator.eq A_ x y orelse memberl A_ x ys
+fun memberl A_ x (y :: ys) = HOL.eq A_ x y orelse memberl A_ x ys
   | memberl A_ x [] = false;
 
 end; (*struct List*)
diff -r 9ef65be6bb2a -r 9886802cbbd6 doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.ML	Tue Jun 05 15:16:10 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/tree.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
 
@@ -8,15 +16,13 @@
 fun less_eq (A_:'a ord) = #less_eq A_;
 fun less (A_:'a ord) = #less A_;
 
-end; (*struct Orderings*)
-
-structure Code_Generator = 
-struct
+type 'a order = {Orderings__order_ord : 'a ord};
+fun order_ord (A_:'a order) = #Orderings__order_ord A_;
 
-type 'a eq = {eq : 'a -> 'a -> bool};
-fun eq (A_:'a eq) = #eq A_;
+type 'a linorder = {Orderings__linorder_order : 'a order};
+fun linorder_order (A_:'a linorder) = #Orderings__linorder_order A_;
 
-end; (*struct Code_Generator*)
+end; (*struct Orderings*)
 
 structure Nat = 
 struct
@@ -28,7 +34,7 @@
   | eq_nat (Suc n) (Suc m) = eq_nat n m
   | eq_nat Zero_nat Zero_nat = true;
 
-val eq_nata = {eq = eq_nat} : nat Code_Generator.eq;
+val eq_nata = {eq = eq_nat} : nat HOL.eq;
 
 fun less_nat n (Suc m) = less_eq_nat n m
   | less_nat n Zero_nat = false
@@ -38,6 +44,11 @@
 val ord_nat = {less_eq = less_eq_nat, less = less_nat} :
   nat Orderings.ord;
 
+val order_nat = {Orderings__order_ord = ord_nat} : nat Orderings.order;
+
+val linorder_nat = {Orderings__linorder_order = order_nat} :
+  nat Orderings.linorder;
+
 end; (*struct Nat*)
 
 structure Codegen = 
@@ -47,23 +58,26 @@
   Branch of ('a, 'b) searchtree * 'a * ('a, 'b) searchtree;
 
 fun update (C1_, C2_) (it, entry) (Branch (t1, key, t2)) =
-  (if Orderings.less_eq C2_ it key
+  (if Orderings.less_eq
+        ((Orderings.order_ord o Orderings.linorder_order) C2_) it key
     then Branch (update (C1_, C2_) (it, entry) t1, key, t2)
     else Branch (t1, key, update (C1_, C2_) (it, entry) t2))
   | update (C1_, C2_) (it, entry) (Leaf (key, vala)) =
-    (if Code_Generator.eq C1_ it key then Leaf (key, entry)
-      else (if Orderings.less_eq C2_ it key
+    (if HOL.eq C1_ it key then Leaf (key, entry)
+      else (if Orderings.less_eq
+                 ((Orderings.order_ord o Orderings.linorder_order) C2_) it
+                 key
              then Branch (Leaf (it, entry), it, Leaf (key, vala))
              else Branch (Leaf (key, vala), it, Leaf (it, entry))));
 
 val example : (Nat.nat, (Nat.nat list)) searchtree =
-  update (Nat.eq_nata, Nat.ord_nat)
+  update (Nat.eq_nata, Nat.linorder_nat)
     (Nat.Suc (Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat))),
       [Nat.Suc (Nat.Suc Nat.Zero_nat), Nat.Suc (Nat.Suc Nat.Zero_nat)])
-    (update (Nat.eq_nata, Nat.ord_nat)
+    (update (Nat.eq_nata, Nat.linorder_nat)
       (Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat)),
         [Nat.Suc (Nat.Suc (Nat.Suc Nat.Zero_nat))])
-      (update (Nat.eq_nata, Nat.ord_nat)
+      (update (Nat.eq_nata, Nat.linorder_nat)
         (Nat.Suc (Nat.Suc Nat.Zero_nat), [Nat.Suc (Nat.Suc Nat.Zero_nat)])
         (Leaf (Nat.Suc Nat.Zero_nat, []))));