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