--- a/src/HOL/ex/InductiveInvariant_examples.thy Fri May 12 10:38:00 2006 +0200
+++ b/src/HOL/ex/InductiveInvariant_examples.thy Fri May 12 11:19:41 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 measure_def inv_image_def)
+apply (auto simp add: indinv_def inv_image_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 measure_def inv_image_def)
+ simp add: ninety_one_tc inv_image_def)
end