diff -r 9afd9b9c47d0 -r c40ce2de2020 src/HOL/ex/InductiveInvariant_examples.thy
--- a/src/HOL/ex/InductiveInvariant_examples.thy	Sun Jun 04 10:52:47 2006 +0200
+++ b/src/HOL/ex/InductiveInvariant_examples.thy	Mon Jun 05 14:22:58 2006 +0200
@@ -105,7 +105,7 @@
 lemma ninety_one_inv: "n < ninety_one n + 11"
 apply (rule_tac x=n in tfl_indinv_wfrec [OF ninety_one_def])
 apply force
-apply (auto simp add: indinv_def inv_image_def)
+apply (auto simp add: indinv_def)
 apply (frule_tac x="x+11" in spec)
 apply (frule_tac x="f (x + 11)" in spec)
 by arith
@@ -125,6 +125,6 @@
                    then x - 10
                    else ninety_one (ninety_one (x+11)))"
 by (subst ninety_one.simps,
-    simp add: ninety_one_tc inv_image_def)
+    simp add: ninety_one_tc)
 
 end