added pos/negDivAlg_induct declarations (from Main.thy);

--- a/src/ZF/Integ/IntDiv.thy	Mon Oct 17 23:10:22 2005 +0200
+++ b/src/ZF/Integ/IntDiv.thy	Mon Oct 17 23:10:23 2005 +0200
@@ -438,7 +438,7 @@
 done
 
 
-lemma posDivAlg_induct:
+lemma posDivAlg_induct [consumes 2]:
   assumes u_int: "u \<in> int"
       and v_int: "v \<in> int"
       and ih: "!!a b. [| a \<in> int; b \<in> int;
@@ -598,7 +598,7 @@
 apply (simp add: not_zle_iff_zless negDivAlg_termination)
 done
 
-lemma negDivAlg_induct:
+lemma negDivAlg_induct [consumes 2]:
   assumes u_int: "u \<in> int"
       and v_int: "v \<in> int"
       and ih: "!!a b. [| a \<in> int; b \<in> int;