# HG changeset patch
# User haftmann
# Date 1241706154 -7200
# Node ID 1d117af9f9f36237d72a93be3eeb1499c416ff92
# Parent  75d7c7cc8bdb2092d61b42472195bcde3db7f8f7
better to have distinguished class for preorders

diff -r 75d7c7cc8bdb -r 1d117af9f9f3 src/HOL/Library/Preorder.thy
--- a/src/HOL/Library/Preorder.thy	Thu May 07 12:17:17 2009 +0200
+++ b/src/HOL/Library/Preorder.thy	Thu May 07 16:22:34 2009 +0200
@@ -6,7 +6,7 @@
 imports Orderings
 begin
 
-context preorder
+class preorder_equiv = preorder
 begin
 
 definition equiv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where