1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML	Tue Mar 18 20:33:33 2008 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/monotype.ML	Tue Mar 18 20:34:26 2008 +0100
     1.3 @@ -8,44 +8,17 @@
     1.4    | eqop_nat Zero_nat (Suc a) = false
     1.5    | eqop_nat (Suc a) Zero_nat = false;
     1.6  
     1.7 -fun plus_nat (Suc m) n = plus_nat m (Suc n)
     1.8 -  | plus_nat Zero_nat n = n;
     1.9 -
    1.10  end; (*struct Nat*)
    1.11  
    1.12 -structure Product_Type = 
    1.13 -struct
    1.14 -
    1.15 -fun split c (a, b) = c a b;
    1.16 -
    1.17 -end; (*struct Product_Type*)
    1.18 -
    1.19  structure List = 
    1.20  struct
    1.21  
    1.22 -fun list_case f1 f2 [] = f1
    1.23 -  | list_case f1 f2 (a :: lista) = f2 a lista;
    1.24 -
    1.25 -fun zip xs (y :: ys) =
    1.26 -  (case xs of [] => [] | z :: zs => (z, y) :: zip zs ys)
    1.27 -  | zip xs [] = [];
    1.28 -
    1.29  fun null (x :: xs) = false
    1.30    | null [] = true;
    1.31  
    1.32 -fun list_all p (x :: xs) = p x andalso list_all p xs
    1.33 -  | list_all p [] = true;
    1.34 -
    1.35 -fun size_list (a :: lista) =
    1.36 -  Nat.plus_nat (size_list lista) (Nat.Suc Nat.Zero_nat)
    1.37 -  | size_list [] = Nat.Zero_nat;
    1.38 -
    1.39  fun list_all2 p (x :: xs) (y :: ys) = p x y andalso list_all2 p xs ys
    1.40    | list_all2 p xs [] = null xs
    1.41 -  | list_all2 p [] ys = null ys
    1.42 -  | list_all2 p xs ys =
    1.43 -    Nat.eqop_nat (size_list xs) (size_list ys) andalso
    1.44 -      list_all (fn a as (aa, b) => p aa b) (zip xs ys);
    1.45 +  | list_all2 p [] ys = null ys;
    1.46  
    1.47  end; (*struct List*)
    1.48