src/HOL/HoareParallel/RG_Examples.thy
changeset 13517 42efec18f5b2
parent 13187 e5434b822a96
child 13601 fd3e3d6b37b2
     1.1 --- a/src/HOL/HoareParallel/RG_Examples.thy	Fri Aug 23 07:34:20 2002 +0200
     1.2 +++ b/src/HOL/HoareParallel/RG_Examples.thy	Fri Aug 23 07:41:05 2002 +0200
     1.3 @@ -278,14 +278,14 @@
     1.4  
     1.5  lemma mod_aux :"\<lbrakk>i < (n::nat); a mod n = i;  j < a + n; j mod n = i; a < j\<rbrakk> \<Longrightarrow> False"
     1.6  apply(subgoal_tac "a=a div n*n + a mod n" )
     1.7 - prefer 2 apply (simp (no_asm_use) only: mod_div_equality [symmetric])
     1.8 + prefer 2 apply (simp (no_asm_use))
     1.9  apply(subgoal_tac "j=j div n*n + j mod n")
    1.10 - prefer 2 apply (simp (no_asm_use) only: mod_div_equality [symmetric])
    1.11 + prefer 2 apply (simp (no_asm_use))
    1.12  apply simp
    1.13  apply(subgoal_tac "a div n*n < j div n*n")
    1.14  prefer 2 apply arith
    1.15  apply(subgoal_tac "j div n*n < (a div n + 1)*n")
    1.16 -prefer 2 apply simp 
    1.17 +prefer 2 apply simp
    1.18  apply (simp only:mult_less_cancel2)
    1.19  apply arith
    1.20  done