author | berghofe |
Mon, 19 Oct 2009 16:45:52 +0200 | |
changeset 33000 | d31a52dbe91e |
parent 32999 | d603c567170b |
child 33001 | 82382652e5e7 |
--- 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)