src/HOL/Orderings.thy
changeset 28823 dcbef866c9e2
parent 28685 275122631271
child 29580 117b88da143c
     1.1 --- a/src/HOL/Orderings.thy	Mon Nov 17 17:00:27 2008 +0100
     1.2 +++ b/src/HOL/Orderings.thy	Mon Nov 17 17:00:55 2008 +0100
     1.3 @@ -71,7 +71,7 @@
     1.4  
     1.5  lemma dual_preorder:
     1.6    "preorder (op \<ge>) (op >)"
     1.7 -by unfold_locales (auto simp add: less_le_not_le intro: order_trans)
     1.8 +proof qed (auto simp add: less_le_not_le intro: order_trans)
     1.9  
    1.10  end
    1.11