# HG changeset patch
# User wenzelm
# Date 1003082550 -7200
# Node ID 8941d8d15dc82f19d61e25955486c0d841005a0c
# Parent  89cff5bfe3b164591d1feed6e0b74bb07cdedebe
removed Ord;

diff -r 89cff5bfe3b1 -r 8941d8d15dc8 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sun Oct 14 20:02:11 2001 +0200
+++ b/src/HOL/Set.thy	Sun Oct 14 20:02:30 2001 +0200
@@ -4,7 +4,7 @@
     Copyright   1993  University of Cambridge
 *)
 
-Set = Ord +
+Set = HOL +
 
 
 (** Core syntax **)