src/HOL/Hoare/Examples.thy
changeset 42154 478bdcea240a
parent 35316 870dfea4f9c0
child 58860 fee7cfa69c50
     1.1 --- a/src/HOL/Hoare/Examples.thy	Tue Mar 29 21:48:01 2011 +0200
     1.2 +++ b/src/HOL/Hoare/Examples.thy	Tue Mar 29 22:36:56 2011 +0200
     1.3 @@ -90,7 +90,7 @@
     1.4   {c = A^B}"
     1.5  apply vcg_simp
     1.6  apply(case_tac "b")
     1.7 - apply(simp add: mod_less)
     1.8 + apply simp
     1.9  apply simp
    1.10  done
    1.11