# HG changeset patch
# User wenzelm
# Date 1129583423 -7200
# Node ID a1f797ff091e237c163d5c3d5e334c690646eb1f
# Parent  805eca99d3986df3c5e3595bbe126cfe6ed9ae76
added pos/negDivAlg_induct declarations (from Main.thy);

diff -r 805eca99d398 -r a1f797ff091e src/ZF/Integ/IntDiv.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;