src/ZF/Integ/IntDiv.thy

 apply auto
 apply (simp add: not_zle_iff_zless posDivAlg_termination)
 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;
                      ~ (a $< b | b $<= #0) --> P(a, #2 $* b) |] ==> P(a,b)"
   shows "P(u,v)"

 apply (drule_tac [3] x = "<xa, #2 $\<times> y>" in spec)
 apply auto
 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;  
                          ~ (#0 $<= a $+ b | b $<= #0) --> P(a, #2 $* b) |]  
                       ==> P(a,b)"