Removed unneeded reference to inv_def.
authorberghofe
Mon, 19 Oct 2009 16:45:52 +0200
changeset 33000 d31a52dbe91e
parent 32999 d603c567170b
child 33001 82382652e5e7
Removed unneeded reference to inv_def.
src/HOL/ex/LocaleTest2.thy
--- a/src/HOL/ex/LocaleTest2.thy	Mon Oct 19 16:45:00 2009 +0200
+++ b/src/HOL/ex/LocaleTest2.thy	Mon Oct 19 16:45:52 2009 +0200
@@ -897,7 +897,7 @@
 apply simp
 done
   show "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
-apply (unfold Dmonoid.inv_def [OF Dmonoid] inv_def)
+apply (unfold Dmonoid.inv_def [OF Dmonoid])
 apply (insert unit_id)
 apply simp
 apply (rule the_equality)