# HG changeset patch
# User paulson
# Date 906722287 -7200
# Node ID 426c1e330903a66c94d9a026c6ab62e789d629d2
# Parent  c17471a9c99c71204305e9e9dd8b5605408d077e
Renaming of Integ/Integ.* to Integ/Int.*, and renaming of related constants

diff -r c17471a9c99c -r 426c1e330903 src/ZF/Integ/Bin.ML
--- a/src/ZF/Integ/Bin.ML	Fri Sep 25 12:12:07 1998 +0200
+++ b/src/ZF/Integ/Bin.ML	Fri Sep 25 13:18:07 1998 +0200
@@ -99,8 +99,8 @@
 
 val bin_typechecks0 = bin_rec_type :: bin.intrs;
 
-Goalw [integ_of_def] "w: bin ==> integ_of(w) : integ";
-by (typechk_tac (bin_typechecks0@integ_typechecks@
+Goalw [integ_of_def] "w: bin ==> integ_of(w) : int";
+by (typechk_tac (bin_typechecks0@int_typechecks@
                  nat_typechecks@[bool_into_nat]));
 qed "integ_of_type";
 
@@ -143,33 +143,13 @@
 	   bin_rec_Pls, bin_rec_Min, bin_rec_Cons] @ 
 	  bin_recs integ_of_def @ bin_typechecks);
 
-val typechecks = bin_typechecks @ integ_typechecks @ nat_typechecks @
+val typechecks = bin_typechecks @ int_typechecks @ nat_typechecks @
                  [bool_subset_nat RS subsetD];
 
 (**** The carry/borrow functions, bin_succ and bin_pred ****)
 
-(** Lemmas **)
-
-goal Integ.thy 
-    "!!z v. [| z $+ v = z' $+ v';  \
-\       z: integ; z': integ;  v: integ; v': integ;  w: integ |]   \
-\    ==> z $+ (v $+ w) = z' $+ (v' $+ w)";
-by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
-qed "zadd_assoc_cong";
-
-goal Integ.thy 
-    "!!z v w. [| z: integ;  v: integ;  w: integ |]   \
-\    ==> z $+ (v $+ w) = v $+ (z $+ w)";
-by (REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1));
-qed "zadd_assoc_swap";
-
-(*Pushes 'constants' of the form $#m to the right -- LOOPS if two!*)
-bind_thm ("zadd_assoc_znat", (znat_type RS zadd_assoc_swap));
-
-
 Addsimps (bin_recs bin_succ_def @ bin_recs bin_pred_def);
 
-
 (*NCons preserves the integer value of its argument*)
 Goal "[| w: bin; b: bool |] ==>     \
 \         integ_of(NCons(w,b)) = integ_of(Cons(w,b))";
@@ -346,7 +326,7 @@
 (*** The computation simpset ***)
 
 (*Adding the typechecking rules as rewrites is much slower, unfortunately...*)
-val bin_comp_ss = simpset_of Integ.thy 
+val bin_comp_ss = simpset_of Int.thy 
     addsimps [integ_of_add RS sym,   (*invoke bin_add*)
               integ_of_minus RS sym, (*invoke bin_minus*)
               integ_of_mult RS sym,  (*invoke bin_mult*)
diff -r c17471a9c99c -r 426c1e330903 src/ZF/Integ/Bin.thy
--- a/src/ZF/Integ/Bin.thy	Fri Sep 25 12:12:07 1998 +0200
+++ b/src/ZF/Integ/Bin.thy	Fri Sep 25 13:18:07 1998 +0200
@@ -18,7 +18,7 @@
 Division is not defined yet!
 *)
 
-Bin = Integ + Datatype + 
+Bin = Int + Datatype + 
 
 consts
   bin_rec   :: [i, i, i, [i,i,i]=>i] => i
@@ -143,15 +143,15 @@
         | bin_of (Const ("Cons", _) $ bs $ b) = dest_bit b :: bin_of bs
         | bin_of _ = raise Match;
 
-      fun int_of [] = 0
-        | int_of (b :: bs) = b + 2 * int_of bs;
+      fun integ_of [] = 0
+        | integ_of (b :: bs) = b + 2 * integ_of bs;
 
       val rev_digs = bin_of tm;
       val (sign, zs) =
         (case rev rev_digs of
           ~1 :: bs => ("-", prefix_len (equal 1) bs)
         | bs => ("", prefix_len (equal 0) bs));
-      val num = string_of_int (abs (int_of rev_digs));
+      val num = string_of_int (abs (integ_of rev_digs));
     in
       "#" ^ sign ^ implode (replicate zs "0") ^ num
     end;
diff -r c17471a9c99c -r 426c1e330903 src/ZF/Integ/Int.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Integ/Int.ML	Fri Sep 25 13:18:07 1998 +0200
@@ -0,0 +1,412 @@
+(*  Title:      ZF/Integ/Int.ML
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+The integers as equivalence classes over nat*nat.
+
+Could also prove...
+"znegative(z) ==> $# zmagnitude(z) = $~ z"
+"~ znegative(z) ==> $# zmagnitude(z) = z"
+$< is a linear ordering
+$+ and $* are monotonic wrt $<
+*)
+
+AddSEs [quotientE];
+
+(*** Proving that intrel is an equivalence relation ***)
+
+(*By luck, requires no typing premises for y1, y2,y3*)
+val eqa::eqb::prems = goal Arith.thy 
+    "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2;  \
+\       x1: nat; x2: nat; x3: nat |]    ==>    x1 #+ y3 = x3 #+ y1";
+by (res_inst_tac [("k","x2")] add_left_cancel 1);
+by (resolve_tac prems 2);
+by (rtac (add_left_commute RS trans) 1 THEN typechk_tac prems);
+by (stac eqb 1);
+by (rtac (add_left_commute RS trans) 1 THEN typechk_tac prems);
+by (stac eqa 1);
+by (rtac (add_left_commute) 1 THEN typechk_tac prems);
+qed "int_trans_lemma";
+
+(** Natural deduction for intrel **)
+
+Goalw [intrel_def]
+    "<<x1,y1>,<x2,y2>>: intrel <-> \
+\    x1: nat & y1: nat & x2: nat & y2: nat & x1#+y2 = x2#+y1";
+by (Fast_tac 1);
+qed "intrel_iff";
+
+Goalw [intrel_def]
+    "[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
+\             <<x1,y1>,<x2,y2>>: intrel";
+by (fast_tac (claset() addIs prems) 1);
+qed "intrelI";
+
+(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
+Goalw [intrel_def]
+  "p: intrel --> (EX x1 y1 x2 y2. \
+\                  p = <<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1 & \
+\                  x1: nat & y1: nat & x2: nat & y2: nat)";
+by (Fast_tac 1);
+qed "intrelE_lemma";
+
+val [major,minor] = goal thy
+  "[| p: intrel;  \
+\     !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>;  x1#+y2 = x2#+y1; \
+\                       x1: nat; y1: nat; x2: nat; y2: nat |] ==> Q |] \
+\  ==> Q";
+by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1);
+by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
+qed "intrelE";
+
+AddSIs [intrelI];
+AddSEs [intrelE];
+
+Goalw [equiv_def, refl_def, sym_def, trans_def]
+    "equiv(nat*nat, intrel)";
+by (fast_tac (claset() addSEs [sym, int_trans_lemma]) 1);
+qed "equiv_intrel";
+
+
+Addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff,
+	  add_0_right, add_succ_right];
+Addcongs [conj_cong];
+
+val eq_intrelD = equiv_intrel RSN (2,eq_equiv_class);
+
+(** int_of: the injection from nat to int **)
+
+Goalw [int_def,quotient_def,int_of_def]
+    "m : nat ==> $#m : int";
+by (fast_tac (claset() addSIs [nat_0I]) 1);
+qed "int_of_type";
+
+Addsimps [int_of_type];
+
+Goalw [int_of_def] "[| $#m = $#n;  m: nat |] ==> m=n";
+by (dtac (sym RS eq_intrelD) 1);
+by (typechk_tac [nat_0I, SigmaI]);
+by (Asm_full_simp_tac 1);
+qed "int_of_inject";
+
+AddSDs [int_of_inject];
+
+Goal "m: nat ==> ($# m = $# n) <-> (m = n)"; 
+by (Blast_tac 1); 
+qed "int_of_eq"; 
+Addsimps [int_of_eq]; 
+
+(**** zminus: unary negation on int ****)
+
+Goalw [congruent_def] "congruent(intrel, %<x,y>. intrel``{<y,x>})";
+by Safe_tac;
+by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
+qed "zminus_congruent";
+
+(*Resolve th against the corresponding facts for zminus*)
+val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
+
+Goalw [int_def,zminus_def] "z : int ==> $~z : int";
+by (typechk_tac [split_type, SigmaI, zminus_ize UN_equiv_class_type,
+                 quotientI]);
+qed "zminus_type";
+
+Goalw [int_def,zminus_def] "[| $~z = $~w;  z: int;  w: int |] ==> z=w";
+by (etac (zminus_ize UN_equiv_class_inject) 1);
+by Safe_tac;
+(*The setloop is only needed because assumptions are in the wrong order!*)
+by (asm_full_simp_tac (simpset() addsimps add_ac
+                       setloop dtac eq_intrelD) 1);
+qed "zminus_inject";
+
+Goalw [zminus_def]
+    "[| x: nat;  y: nat |] ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
+by (asm_simp_tac (simpset() addsimps [zminus_ize UN_equiv_class, SigmaI]) 1);
+qed "zminus";
+
+Goalw [int_def] "z : int ==> $~ ($~ z) = z";
+by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
+by (asm_simp_tac (simpset() addsimps [zminus]) 1);
+qed "zminus_zminus";
+
+Goalw [int_def, int_of_def] "$~ ($#0) = $#0";
+by (simp_tac (simpset() addsimps [zminus]) 1);
+qed "zminus_0";
+
+Addsimps [zminus_zminus, zminus_0];
+
+
+(**** znegative: the test for negative integers ****)
+
+(*No natural number is negative!*)
+Goalw [znegative_def, int_of_def]  "~ znegative($# n)";
+by Safe_tac;
+by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1);
+by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1);
+by (force_tac (claset(),
+	       simpset() addsimps [add_le_self2 RS le_imp_not_lt]) 1);
+qed "not_znegative_int_of";
+
+Addsimps [not_znegative_int_of];
+AddSEs   [not_znegative_int_of RS notE];
+
+Goalw [znegative_def, int_of_def] "n: nat ==> znegative($~ $# succ(n))";
+by (asm_simp_tac (simpset() addsimps [zminus]) 1);
+by (blast_tac (claset() addIs [nat_0_le]) 1);
+qed "znegative_zminus_int_of";
+
+Addsimps [znegative_zminus_int_of];
+
+Goalw [znegative_def, int_of_def] "[| n: nat; ~ znegative($~ $# n) |] ==> n=0";
+by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1);
+be natE 1;
+by (dres_inst_tac [("x","0")] spec 2);
+by Auto_tac;
+qed "not_znegative_imp_zero";
+
+(**** zmagnitude: magnitide of an integer, as a natural number ****)
+
+Goalw [zmagnitude_def] "n: nat ==> zmagnitude($# n) = n";
+by Auto_tac;
+qed "zmagnitude_int_of";
+
+Goalw [zmagnitude_def] "n: nat ==> zmagnitude($~ $# n) = n";
+by (auto_tac(claset() addDs [not_znegative_imp_zero], simpset()));
+qed "zmagnitude_zminus_int_of";
+
+Addsimps [zmagnitude_int_of, zmagnitude_zminus_int_of];
+
+Goalw [zmagnitude_def] "zmagnitude(z) : nat";
+br theI2 1;
+by Auto_tac;
+qed "zmagnitude_type";
+
+Goalw [int_def, znegative_def, int_of_def]
+     "[| z: int; ~ znegative(z) |] ==> EX n:nat. z = $# n"; 
+by (auto_tac(claset() , simpset() addsimps [image_singleton_iff]));
+by (rename_tac "i j" 1);
+by (dres_inst_tac [("x", "i")] spec 1);
+by (dres_inst_tac [("x", "j")] spec 1);
+br bexI 1;
+br (add_diff_inverse2 RS sym) 1;
+by Auto_tac;
+by (asm_full_simp_tac (simpset() addsimps [nat_into_Ord, not_lt_iff_le]) 1);
+qed "not_zneg_int_of";
+
+Goal "[| z: int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"; 
+bd not_zneg_int_of 1;
+by Auto_tac;
+qed "not_zneg_mag"; 
+
+Addsimps [not_zneg_mag];
+
+
+Goalw [int_def, znegative_def, int_of_def]
+     "[| z: int; znegative(z) |] ==> EX n:nat. z = $~ ($# succ(n))"; 
+by (auto_tac(claset() addSDs [less_imp_Suc_add], 
+	     simpset() addsimps [zminus, image_singleton_iff]));
+by (rename_tac "m n j k" 1);
+by (subgoal_tac "j #+ succ(m #+ k) = j #+ n" 1);
+by (rotate_tac ~2 2);
+by (asm_full_simp_tac (simpset() addsimps add_ac) 2);
+by (blast_tac (claset() addSDs [add_left_cancel]) 1);
+qed "zneg_int_of";
+
+Goal "[| z: int; znegative(z) |] ==> $# (zmagnitude(z)) = $~ z"; 
+bd zneg_int_of 1;
+by Auto_tac;
+qed "zneg_mag"; 
+
+Addsimps [zneg_mag];
+
+
+(**** zadd: addition on int ****)
+
+(** Congruence property for addition **)
+
+Goalw [congruent2_def]
+    "congruent2(intrel, %z1 z2.                      \
+\         let <x1,y1>=z1; <x2,y2>=z2                 \
+\                           in intrel``{<x1#+x2, y1#+y2>})";
+(*Proof via congruent2_commuteI seems longer*)
+by Safe_tac;
+by (asm_simp_tac (simpset() addsimps [add_assoc, Let_def]) 1);
+(*The rest should be trivial, but rearranging terms is hard;
+  add_ac does not help rewriting with the assumptions.*)
+by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1);
+by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 3);
+by (typechk_tac [add_type]);
+by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
+qed "zadd_congruent2";
+
+(*Resolve th against the corresponding facts for zadd*)
+val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
+
+Goalw [int_def,zadd_def] "[| z: int;  w: int |] ==> z $+ w : int";
+by (rtac (zadd_ize UN_equiv_class_type2) 1);
+by (simp_tac (simpset() addsimps [Let_def]) 3);
+by (REPEAT (ares_tac [split_type, add_type, quotientI, SigmaI] 1));
+qed "zadd_type";
+
+Goalw [zadd_def]
+  "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==>       \
+\           (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) =        \
+\           intrel `` {<x1#+x2, y1#+y2>}";
+by (asm_simp_tac (simpset() addsimps [zadd_ize UN_equiv_class2, SigmaI]) 1);
+by (simp_tac (simpset() addsimps [Let_def]) 1);
+qed "zadd";
+
+Goalw [int_def,int_of_def] "z : int ==> $#0 $+ z = z";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+by (asm_simp_tac (simpset() addsimps [zadd]) 1);
+qed "zadd_0";
+
+Goalw [int_def] "[| z: int;  w: int |] ==> $~ (z $+ w) = $~ z $+ $~ w";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1);
+qed "zminus_zadd_distrib";
+
+Goalw [int_def] "[| z: int;  w: int |] ==> z $+ w = w $+ z";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+by (asm_simp_tac (simpset() addsimps add_ac @ [zadd]) 1);
+qed "zadd_commute";
+
+Goalw [int_def]
+    "[| z1: int;  z2: int;  z3: int |]   \
+\    ==> (z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+(*rewriting is much faster without intrel_iff, etc.*)
+by (asm_simp_tac (simpset() addsimps [zadd, add_assoc]) 1);
+qed "zadd_assoc";
+
+(*For AC rewriting*)
+Goal "[| z1:int;  z2:int;  z3: int |] ==> z1$+(z2$+z3) = z2$+(z1$+z3)";
+by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym, zadd_commute]) 1);
+qed "zadd_left_commute";
+
+(*Integer addition is an AC operator*)
+val zadd_ac = [zadd_assoc, zadd_commute, zadd_left_commute];
+
+Goalw [int_of_def]
+    "[| m: nat;  n: nat |] ==> $# (m #+ n) = ($#m) $+ ($#n)";
+by (asm_simp_tac (simpset() addsimps [zadd]) 1);
+qed "int_of_add";
+
+Goalw [int_def,int_of_def] "z : int ==> z $+ ($~ z) = $#0";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1);
+qed "zadd_zminus_inverse";
+
+Goal "z : int ==> ($~ z) $+ z = $#0";
+by (asm_simp_tac
+    (simpset() addsimps [zadd_commute, zminus_type, zadd_zminus_inverse]) 1);
+qed "zadd_zminus_inverse2";
+
+Goal "z:int ==> z $+ $#0 = z";
+by (rtac (zadd_commute RS trans) 1);
+by (REPEAT (ares_tac [int_of_type, nat_0I, zadd_0] 1));
+qed "zadd_0_right";
+
+Addsimps [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2];
+
+
+(*Need properties of $- ???  Or use $- just as an abbreviation?
+     [| m: nat;  n: nat;  m>=n |] ==> $# (m #- n) = ($#m) $- ($#n)
+*)
+
+(**** zmult: multiplication on int ****)
+
+(** Congruence property for multiplication **)
+
+Goal "congruent2(intrel, %p1 p2.                 \
+\               split(%x1 y1. split(%x2 y2.     \
+\                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))";
+by (rtac (equiv_intrel RS congruent2_commuteI) 1);
+by Safe_tac;
+by (ALLGOALS Asm_simp_tac);
+(*Proof that zmult is congruent in one argument*)
+by (asm_simp_tac 
+    (simpset() addsimps add_ac @ [add_mult_distrib_left RS sym]) 2);
+by (asm_simp_tac
+    (simpset() addsimps [add_assoc RS sym, add_mult_distrib_left RS sym]) 2);
+(*Proof that zmult is commutative on representatives*)
+by (asm_simp_tac (simpset() addsimps mult_ac@add_ac) 1);
+qed "zmult_congruent2";
+
+
+(*Resolve th against the corresponding facts for zmult*)
+val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
+
+Goalw [int_def,zmult_def] "[| z: int;  w: int |] ==> z $* w : int";
+by (REPEAT (ares_tac [zmult_ize UN_equiv_class_type2,
+                      split_type, add_type, mult_type, 
+                      quotientI, SigmaI] 1));
+qed "zmult_type";
+
+Goalw [zmult_def]
+     "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==>    \
+\              (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) =     \
+\              intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
+by (asm_simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2, SigmaI]) 1);
+qed "zmult";
+
+Goalw [int_def,int_of_def] "z : int ==> $#0 $* z = $#0";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+by (asm_simp_tac (simpset() addsimps [zmult]) 1);
+qed "zmult_0";
+
+Goalw [int_def,int_of_def] "z : int ==> $#1 $* z = z";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+by (asm_simp_tac (simpset() addsimps [zmult, add_0_right]) 1);
+qed "zmult_1";
+
+Goalw [int_def] "[| z: int;  w: int |] ==> ($~ z) $* w = $~ (z $* w)";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
+qed "zmult_zminus";
+
+Addsimps [zmult_0, zmult_1, zmult_zminus];
+
+Goalw [int_def] "[| z: int;  w: int |] ==> ($~ z) $* ($~ w) = (z $* w)";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
+qed "zmult_zminus_zminus";
+
+Goalw [int_def] "[| z: int;  w: int |] ==> z $* w = w $* z";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+by (asm_simp_tac (simpset() addsimps [zmult] @ add_ac @ mult_ac) 1);
+qed "zmult_commute";
+
+Goalw [int_def]
+    "[| z1: int;  z2: int;  z3: int |]     \
+\    ==> (z1 $* z2) $* z3 = z1 $* (z2 $* z3)";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+by (asm_simp_tac 
+    (simpset() addsimps [zmult, add_mult_distrib_left, 
+                         add_mult_distrib] @ add_ac @ mult_ac) 1);
+qed "zmult_assoc";
+
+(*For AC rewriting*)
+Goal "[| z1:int;  z2:int;  z3: int |] ==> z1$*(z2$*z3) = z2$*(z1$*z3)";
+by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym, zmult_commute]) 1);
+qed "zmult_left_commute";
+
+(*Integer multiplication is an AC operator*)
+val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
+
+Goalw [int_def]
+    "[| z1: int;  z2: int;  w: int |] ==> \
+\                (z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)";
+by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
+by (asm_simp_tac (simpset() addsimps [zadd, zmult, add_mult_distrib]) 1);
+by (asm_simp_tac (simpset() addsimps add_ac @ mult_ac) 1);
+qed "zadd_zmult_distrib";
+
+val int_typechecks =
+    [int_of_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
+
+Addsimps int_typechecks;
+
+
+
diff -r c17471a9c99c -r 426c1e330903 src/ZF/Integ/Int.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Integ/Int.thy	Fri Sep 25 13:18:07 1998 +0200
@@ -0,0 +1,60 @@
+(*  Title:      ZF/Integ/Int.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1993  University of Cambridge
+
+The integers as equivalence classes over nat*nat.
+*)
+
+Int = EquivClass + Arith +
+consts
+    intrel,int::      i
+    int_of      ::      i=>i            ("$# _" [80] 80)
+    zminus      ::      i=>i            ("$~ _" [80] 80)
+    znegative   ::      i=>o
+    zmagnitude  ::      i=>i
+    "$*"        ::      [i,i]=>i      (infixl 70)
+    "$'/"       ::      [i,i]=>i      (infixl 70) 
+    "$'/'/"     ::      [i,i]=>i      (infixl 70)
+    "$+"        ::      [i,i]=>i      (infixl 65)
+    "$-"        ::      [i,i]=>i      (infixl 65)
+    "$<"        ::      [i,i]=>o        (infixl 50)
+
+defs
+
+    intrel_def
+     "intrel == {p:(nat*nat)*(nat*nat).                 
+        EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
+
+    int_def   "int == (nat*nat)/intrel"
+    
+    int_of_def  "$# m == intrel `` {<m,0>}"
+    
+    zminus_def  "$~ Z == UN <x,y>:Z. intrel``{<y,x>}"
+    
+    znegative_def
+        "znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
+    
+    zmagnitude_def
+        "zmagnitude(Z) ==
+	 THE m. m : nat & ((~ znegative(Z) & Z = $# m) |
+	                   (znegative(Z) & $~ Z = $# m))"
+    
+    (*Cannot use UN<x1,y2> here or in zmult because of the form of congruent2.
+      Perhaps a "curried" or even polymorphic congruent predicate would be
+      better.*)
+    zadd_def
+     "Z1 $+ Z2 == 
+       UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2                 
+                           in intrel``{<x1#+x2, y1#+y2>}"
+    
+    zdiff_def   "Z1 $- Z2 == Z1 $+ zminus(Z2)"
+    zless_def   "Z1 $< Z2 == znegative(Z1 $- Z2)"
+    
+    (*This illustrates the primitive form of definitions (no patterns)*)
+    zmult_def
+     "Z1 $* Z2 == 
+       UN p1:Z1. UN p2:Z2.  split(%x1 y1. split(%x2 y2.        
+                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
+    
+ end
diff -r c17471a9c99c -r 426c1e330903 src/ZF/Integ/Integ.ML
--- a/src/ZF/Integ/Integ.ML	Fri Sep 25 12:12:07 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,412 +0,0 @@
-(*  Title:      ZF/ex/integ.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
-
-The integers as equivalence classes over nat*nat.
-
-Could also prove...
-"znegative(z) ==> $# zmagnitude(z) = $~ z"
-"~ znegative(z) ==> $# zmagnitude(z) = z"
-$< is a linear ordering
-$+ and $* are monotonic wrt $<
-*)
-
-AddSEs [quotientE];
-
-(*** Proving that intrel is an equivalence relation ***)
-
-(*By luck, requires no typing premises for y1, y2,y3*)
-val eqa::eqb::prems = goal Arith.thy 
-    "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2;  \
-\       x1: nat; x2: nat; x3: nat |]    ==>    x1 #+ y3 = x3 #+ y1";
-by (res_inst_tac [("k","x2")] add_left_cancel 1);
-by (resolve_tac prems 2);
-by (rtac (add_left_commute RS trans) 1 THEN typechk_tac prems);
-by (stac eqb 1);
-by (rtac (add_left_commute RS trans) 1 THEN typechk_tac prems);
-by (stac eqa 1);
-by (rtac (add_left_commute) 1 THEN typechk_tac prems);
-qed "integ_trans_lemma";
-
-(** Natural deduction for intrel **)
-
-Goalw [intrel_def]
-    "<<x1,y1>,<x2,y2>>: intrel <-> \
-\    x1: nat & y1: nat & x2: nat & y2: nat & x1#+y2 = x2#+y1";
-by (Fast_tac 1);
-qed "intrel_iff";
-
-Goalw [intrel_def]
-    "[| x1#+y2 = x2#+y1; x1: nat; y1: nat; x2: nat; y2: nat |] ==> \
-\             <<x1,y1>,<x2,y2>>: intrel";
-by (fast_tac (claset() addIs prems) 1);
-qed "intrelI";
-
-(*intrelE is hard to derive because fast_tac tries hyp_subst_tac so soon*)
-Goalw [intrel_def]
-  "p: intrel --> (EX x1 y1 x2 y2. \
-\                  p = <<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1 & \
-\                  x1: nat & y1: nat & x2: nat & y2: nat)";
-by (Fast_tac 1);
-qed "intrelE_lemma";
-
-val [major,minor] = goal Integ.thy
-  "[| p: intrel;  \
-\     !!x1 y1 x2 y2. [| p = <<x1,y1>,<x2,y2>>;  x1#+y2 = x2#+y1; \
-\                       x1: nat; y1: nat; x2: nat; y2: nat |] ==> Q |] \
-\  ==> Q";
-by (cut_facts_tac [major RS (intrelE_lemma RS mp)] 1);
-by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
-qed "intrelE";
-
-AddSIs [intrelI];
-AddSEs [intrelE];
-
-Goalw [equiv_def, refl_def, sym_def, trans_def]
-    "equiv(nat*nat, intrel)";
-by (fast_tac (claset() addSEs [sym, integ_trans_lemma]) 1);
-qed "equiv_intrel";
-
-
-Addsimps [equiv_intrel RS eq_equiv_class_iff, intrel_iff,
-	  add_0_right, add_succ_right];
-Addcongs [conj_cong];
-
-val eq_intrelD = equiv_intrel RSN (2,eq_equiv_class);
-
-(** znat: the injection from nat to integ **)
-
-Goalw [integ_def,quotient_def,znat_def]
-    "m : nat ==> $#m : integ";
-by (fast_tac (claset() addSIs [nat_0I]) 1);
-qed "znat_type";
-
-Addsimps [znat_type];
-
-Goalw [znat_def] "[| $#m = $#n;  m: nat |] ==> m=n";
-by (dtac (sym RS eq_intrelD) 1);
-by (typechk_tac [nat_0I, SigmaI]);
-by (Asm_full_simp_tac 1);
-qed "znat_inject";
-
-AddSDs [znat_inject];
-
-Goal "m: nat ==> ($# m = $# n) <-> (m = n)"; 
-by (Blast_tac 1); 
-qed "znat_znat_eq"; 
-Addsimps [znat_znat_eq]; 
-
-(**** zminus: unary negation on integ ****)
-
-Goalw [congruent_def] "congruent(intrel, %<x,y>. intrel``{<y,x>})";
-by Safe_tac;
-by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
-qed "zminus_congruent";
-
-(*Resolve th against the corresponding facts for zminus*)
-val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
-
-Goalw [integ_def,zminus_def] "z : integ ==> $~z : integ";
-by (typechk_tac [split_type, SigmaI, zminus_ize UN_equiv_class_type,
-                 quotientI]);
-qed "zminus_type";
-
-Goalw [integ_def,zminus_def] "[| $~z = $~w;  z: integ;  w: integ |] ==> z=w";
-by (etac (zminus_ize UN_equiv_class_inject) 1);
-by Safe_tac;
-(*The setloop is only needed because assumptions are in the wrong order!*)
-by (asm_full_simp_tac (simpset() addsimps add_ac
-                       setloop dtac eq_intrelD) 1);
-qed "zminus_inject";
-
-Goalw [zminus_def]
-    "[| x: nat;  y: nat |] ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
-by (asm_simp_tac (simpset() addsimps [zminus_ize UN_equiv_class, SigmaI]) 1);
-qed "zminus";
-
-Goalw [integ_def] "z : integ ==> $~ ($~ z) = z";
-by (REPEAT (eresolve_tac [quotientE,SigmaE,ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zminus]) 1);
-qed "zminus_zminus";
-
-Goalw [integ_def, znat_def] "$~ ($#0) = $#0";
-by (simp_tac (simpset() addsimps [zminus]) 1);
-qed "zminus_0";
-
-Addsimps [zminus_zminus, zminus_0];
-
-
-(**** znegative: the test for negative integers ****)
-
-(*No natural number is negative!*)
-Goalw [znegative_def, znat_def]  "~ znegative($# n)";
-by Safe_tac;
-by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1);
-by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1);
-by (force_tac (claset(),
-	       simpset() addsimps [add_le_self2 RS le_imp_not_lt]) 1);
-qed "not_znegative_znat";
-
-Addsimps [not_znegative_znat];
-AddSEs   [not_znegative_znat RS notE];
-
-Goalw [znegative_def, znat_def] "n: nat ==> znegative($~ $# succ(n))";
-by (asm_simp_tac (simpset() addsimps [zminus]) 1);
-by (blast_tac (claset() addIs [nat_0_le]) 1);
-qed "znegative_zminus_znat";
-
-Addsimps [znegative_zminus_znat];
-
-Goalw [znegative_def, znat_def] "[| n: nat; ~ znegative($~ $# n) |] ==> n=0";
-by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1);
-be natE 1;
-by (dres_inst_tac [("x","0")] spec 2);
-by Auto_tac;
-qed "not_znegative_imp_zero";
-
-(**** zmagnitude: magnitide of an integer, as a natural number ****)
-
-Goalw [zmagnitude_def] "n: nat ==> zmagnitude($# n) = n";
-by Auto_tac;
-qed "zmagnitude_znat";
-
-Goalw [zmagnitude_def] "n: nat ==> zmagnitude($~ $# n) = n";
-by (auto_tac(claset() addDs [not_znegative_imp_zero], simpset()));
-qed "zmagnitude_zminus_znat";
-
-Addsimps [zmagnitude_znat, zmagnitude_zminus_znat];
-
-Goalw [zmagnitude_def] "zmagnitude(z) : nat";
-br theI2 1;
-by Auto_tac;
-qed "zmagnitude_type";
-
-Goalw [integ_def, znegative_def, znat_def]
-     "[| z: integ; ~ znegative(z) |] ==> EX n:nat. z = $# n"; 
-by (auto_tac(claset() , simpset() addsimps [image_singleton_iff]));
-by (rename_tac "i j" 1);
-by (dres_inst_tac [("x", "i")] spec 1);
-by (dres_inst_tac [("x", "j")] spec 1);
-br bexI 1;
-br (add_diff_inverse2 RS sym) 1;
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [nat_into_Ord, not_lt_iff_le]) 1);
-qed "not_zneg_znat";
-
-Goal "[| z: integ; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"; 
-bd not_zneg_znat 1;
-by Auto_tac;
-qed "not_zneg_mag"; 
-
-Addsimps [not_zneg_mag];
-
-
-Goalw [integ_def, znegative_def, znat_def]
-     "[| z: integ; znegative(z) |] ==> EX n:nat. z = $~ ($# succ(n))"; 
-by (auto_tac(claset() addSDs [less_imp_Suc_add], 
-	     simpset() addsimps [zminus, image_singleton_iff]));
-by (rename_tac "m n j k" 1);
-by (subgoal_tac "j #+ succ(m #+ k) = j #+ n" 1);
-by (rotate_tac ~2 2);
-by (asm_full_simp_tac (simpset() addsimps add_ac) 2);
-by (blast_tac (claset() addSDs [add_left_cancel]) 1);
-qed "zneg_znat";
-
-Goal "[| z: integ; znegative(z) |] ==> $# (zmagnitude(z)) = $~ z"; 
-bd zneg_znat 1;
-by Auto_tac;
-qed "zneg_mag"; 
-
-Addsimps [zneg_mag];
-
-
-(**** zadd: addition on integ ****)
-
-(** Congruence property for addition **)
-
-Goalw [congruent2_def]
-    "congruent2(intrel, %z1 z2.                      \
-\         let <x1,y1>=z1; <x2,y2>=z2                 \
-\                           in intrel``{<x1#+x2, y1#+y2>})";
-(*Proof via congruent2_commuteI seems longer*)
-by Safe_tac;
-by (asm_simp_tac (simpset() addsimps [add_assoc, Let_def]) 1);
-(*The rest should be trivial, but rearranging terms is hard;
-  add_ac does not help rewriting with the assumptions.*)
-by (res_inst_tac [("m1","x1a")] (add_left_commute RS ssubst) 1);
-by (res_inst_tac [("m1","x2a")] (add_left_commute RS ssubst) 3);
-by (typechk_tac [add_type]);
-by (asm_simp_tac (simpset() addsimps [add_assoc RS sym]) 1);
-qed "zadd_congruent2";
-
-(*Resolve th against the corresponding facts for zadd*)
-val zadd_ize = RSLIST [equiv_intrel, zadd_congruent2];
-
-Goalw [integ_def,zadd_def] "[| z: integ;  w: integ |] ==> z $+ w : integ";
-by (rtac (zadd_ize UN_equiv_class_type2) 1);
-by (simp_tac (simpset() addsimps [Let_def]) 3);
-by (REPEAT (ares_tac [split_type, add_type, quotientI, SigmaI] 1));
-qed "zadd_type";
-
-Goalw [zadd_def]
-  "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==>       \
-\           (intrel``{<x1,y1>}) $+ (intrel``{<x2,y2>}) =        \
-\           intrel `` {<x1#+x2, y1#+y2>}";
-by (asm_simp_tac (simpset() addsimps [zadd_ize UN_equiv_class2, SigmaI]) 1);
-by (simp_tac (simpset() addsimps [Let_def]) 1);
-qed "zadd";
-
-Goalw [integ_def,znat_def] "z : integ ==> $#0 $+ z = z";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zadd]) 1);
-qed "zadd_0";
-
-Goalw [integ_def] "[| z: integ;  w: integ |] ==> $~ (z $+ w) = $~ z $+ $~ w";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1);
-qed "zminus_zadd_distrib";
-
-Goalw [integ_def] "[| z: integ;  w: integ |] ==> z $+ w = w $+ z";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps add_ac @ [zadd]) 1);
-qed "zadd_commute";
-
-Goalw [integ_def]
-    "[| z1: integ;  z2: integ;  z3: integ |]   \
-\    ==> (z1 $+ z2) $+ z3 = z1 $+ (z2 $+ z3)";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-(*rewriting is much faster without intrel_iff, etc.*)
-by (asm_simp_tac (simpset() addsimps [zadd, add_assoc]) 1);
-qed "zadd_assoc";
-
-(*For AC rewriting*)
-Goal "[| z1:integ;  z2:integ;  z3: integ |] ==> z1$+(z2$+z3) = z2$+(z1$+z3)";
-by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym, zadd_commute]) 1);
-qed "zadd_left_commute";
-
-(*Integer addition is an AC operator*)
-val zadd_ac = [zadd_assoc, zadd_commute, zadd_left_commute];
-
-Goalw [znat_def]
-    "[| m: nat;  n: nat |] ==> $# (m #+ n) = ($#m) $+ ($#n)";
-by (asm_simp_tac (simpset() addsimps [zadd]) 1);
-qed "znat_add";
-
-Goalw [integ_def,znat_def] "z : integ ==> z $+ ($~ z) = $#0";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1);
-qed "zadd_zminus_inverse";
-
-Goal "z : integ ==> ($~ z) $+ z = $#0";
-by (asm_simp_tac
-    (simpset() addsimps [zadd_commute, zminus_type, zadd_zminus_inverse]) 1);
-qed "zadd_zminus_inverse2";
-
-Goal "z:integ ==> z $+ $#0 = z";
-by (rtac (zadd_commute RS trans) 1);
-by (REPEAT (ares_tac [znat_type, nat_0I, zadd_0] 1));
-qed "zadd_0_right";
-
-Addsimps [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2];
-
-
-(*Need properties of $- ???  Or use $- just as an abbreviation?
-     [| m: nat;  n: nat;  m>=n |] ==> $# (m #- n) = ($#m) $- ($#n)
-*)
-
-(**** zmult: multiplication on integ ****)
-
-(** Congruence property for multiplication **)
-
-Goal "congruent2(intrel, %p1 p2.                 \
-\               split(%x1 y1. split(%x2 y2.     \
-\                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))";
-by (rtac (equiv_intrel RS congruent2_commuteI) 1);
-by Safe_tac;
-by (ALLGOALS Asm_simp_tac);
-(*Proof that zmult is congruent in one argument*)
-by (asm_simp_tac 
-    (simpset() addsimps add_ac @ [add_mult_distrib_left RS sym]) 2);
-by (asm_simp_tac
-    (simpset() addsimps [add_assoc RS sym, add_mult_distrib_left RS sym]) 2);
-(*Proof that zmult is commutative on representatives*)
-by (asm_simp_tac (simpset() addsimps mult_ac@add_ac) 1);
-qed "zmult_congruent2";
-
-
-(*Resolve th against the corresponding facts for zmult*)
-val zmult_ize = RSLIST [equiv_intrel, zmult_congruent2];
-
-Goalw [integ_def,zmult_def] "[| z: integ;  w: integ |] ==> z $* w : integ";
-by (REPEAT (ares_tac [zmult_ize UN_equiv_class_type2,
-                      split_type, add_type, mult_type, 
-                      quotientI, SigmaI] 1));
-qed "zmult_type";
-
-Goalw [zmult_def]
-     "[| x1: nat; y1: nat;  x2: nat; y2: nat |] ==>    \
-\              (intrel``{<x1,y1>}) $* (intrel``{<x2,y2>}) =     \
-\              intrel `` {<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}";
-by (asm_simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2, SigmaI]) 1);
-qed "zmult";
-
-Goalw [integ_def,znat_def] "z : integ ==> $#0 $* z = $#0";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zmult]) 1);
-qed "zmult_0";
-
-Goalw [integ_def,znat_def] "z : integ ==> $#1 $* z = z";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zmult, add_0_right]) 1);
-qed "zmult_1";
-
-Goalw [integ_def] "[| z: integ;  w: integ |] ==> ($~ z) $* w = $~ (z $* w)";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
-qed "zmult_zminus";
-
-Addsimps [zmult_0, zmult_1, zmult_zminus];
-
-Goalw [integ_def] "[| z: integ;  w: integ |] ==> ($~ z) $* ($~ w) = (z $* w)";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
-qed "zmult_zminus_zminus";
-
-Goalw [integ_def] "[| z: integ;  w: integ |] ==> z $* w = w $* z";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zmult] @ add_ac @ mult_ac) 1);
-qed "zmult_commute";
-
-Goalw [integ_def]
-    "[| z1: integ;  z2: integ;  z3: integ |]     \
-\    ==> (z1 $* z2) $* z3 = z1 $* (z2 $* z3)";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac 
-    (simpset() addsimps [zmult, add_mult_distrib_left, 
-                         add_mult_distrib] @ add_ac @ mult_ac) 1);
-qed "zmult_assoc";
-
-(*For AC rewriting*)
-Goal "[| z1:integ;  z2:integ;  z3: integ |] ==> z1$*(z2$*z3) = z2$*(z1$*z3)";
-by (asm_simp_tac (simpset() addsimps [zmult_assoc RS sym, zmult_commute]) 1);
-qed "zmult_left_commute";
-
-(*Integer multiplication is an AC operator*)
-val zmult_ac = [zmult_assoc, zmult_commute, zmult_left_commute];
-
-Goalw [integ_def]
-    "[| z1: integ;  z2: integ;  w: integ |] ==> \
-\                (z1 $+ z2) $* w = (z1 $* w) $+ (z2 $* w)";
-by (REPEAT (eresolve_tac [quotientE, SigmaE, ssubst] 1));
-by (asm_simp_tac (simpset() addsimps [zadd, zmult, add_mult_distrib]) 1);
-by (asm_simp_tac (simpset() addsimps add_ac @ mult_ac) 1);
-qed "zadd_zmult_distrib";
-
-val integ_typechecks =
-    [znat_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
-
-Addsimps integ_typechecks;
-
-
-
diff -r c17471a9c99c -r 426c1e330903 src/ZF/Integ/Integ.thy
--- a/src/ZF/Integ/Integ.thy	Fri Sep 25 12:12:07 1998 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(*  Title:      ZF/ex/integ.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
-
-The integers as equivalence classes over nat*nat.
-*)
-
-Integ = EquivClass + Arith +
-consts
-    intrel,integ::      i
-    znat        ::      i=>i            ("$# _" [80] 80)
-    zminus      ::      i=>i            ("$~ _" [80] 80)
-    znegative   ::      i=>o
-    zmagnitude  ::      i=>i
-    "$*"        ::      [i,i]=>i      (infixl 70)
-    "$'/"       ::      [i,i]=>i      (infixl 70) 
-    "$'/'/"     ::      [i,i]=>i      (infixl 70)
-    "$+"        ::      [i,i]=>i      (infixl 65)
-    "$-"        ::      [i,i]=>i      (infixl 65)
-    "$<"        ::      [i,i]=>o        (infixl 50)
-
-defs
-
-    intrel_def
-     "intrel == {p:(nat*nat)*(nat*nat).                 
-        EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
-
-    integ_def   "integ == (nat*nat)/intrel"
-    
-    znat_def    "$# m == intrel `` {<m,0>}"
-    
-    zminus_def  "$~ Z == UN <x,y>:Z. intrel``{<y,x>}"
-    
-    znegative_def
-        "znegative(Z) == EX x y. x<y & y:nat & <x,y>:Z"
-    
-    zmagnitude_def
-        "zmagnitude(Z) ==
-	 THE m. m : nat & ((~ znegative(Z) & Z = $# m) |
-	                   (znegative(Z) & $~ Z = $# m))"
-    
-    (*Cannot use UN<x1,y2> here or in zmult because of the form of congruent2.
-      Perhaps a "curried" or even polymorphic congruent predicate would be
-      better.*)
-    zadd_def
-     "Z1 $+ Z2 == 
-       UN z1:Z1. UN z2:Z2. let <x1,y1>=z1; <x2,y2>=z2                 
-                           in intrel``{<x1#+x2, y1#+y2>}"
-    
-    zdiff_def   "Z1 $- Z2 == Z1 $+ zminus(Z2)"
-    zless_def   "Z1 $< Z2 == znegative(Z1 $- Z2)"
-    
-    (*This illustrates the primitive form of definitions (no patterns)*)
-    zmult_def
-     "Z1 $* Z2 == 
-       UN p1:Z1. UN p2:Z2.  split(%x1 y1. split(%x2 y2.        
-                   intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1)"
-    
- end
diff -r c17471a9c99c -r 426c1e330903 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Fri Sep 25 12:12:07 1998 +0200
+++ b/src/ZF/IsaMakefile	Fri Sep 25 13:18:07 1998 +0200
@@ -44,7 +44,7 @@
   ind_syntax.ML ind_syntax.thy indrule.ML indrule.thy intr_elim.ML \
   intr_elim.thy mono.ML mono.thy pair.ML pair.thy simpdata.ML subset.ML \
   subset.thy thy_syntax.ML typechk.ML upair.ML upair.thy \
-  Integ/EquivClass.ML Integ/EquivClass.thy Integ/Integ.ML Integ/Integ.thy \
+  Integ/EquivClass.ML Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy \
   Integ/twos_compl.ML Integ/Bin.ML Integ/Bin.thy 
 	@$(ISATOOL) usedir -b $(OUT)/FOL ZF