| changeset 44921 | 58eef4843641 |
| parent 44058 | ae85c5d64913 |
| child 45221 | 3eadb9b6a055 |
--- a/src/HOL/Orderings.thy Tue Sep 13 08:21:51 2011 -0700 +++ b/src/HOL/Orderings.thy Tue Sep 13 17:07:33 2011 -0700 @@ -1309,10 +1309,10 @@ instance "fun" :: (type, preorder) preorder proof qed (auto simp add: le_fun_def less_fun_def - intro: order_trans antisym intro!: ext) + intro: order_trans antisym) instance "fun" :: (type, order) order proof -qed (auto simp add: le_fun_def intro: antisym ext) +qed (auto simp add: le_fun_def intro: antisym) instantiation "fun" :: (type, bot) bot begin