--- a/src/HOL/Orderings.thy Wed Dec 13 14:56:50 2006 +0100 +++ b/src/HOL/Orderings.thy Wed Dec 13 15:45:29 2006 +0100 @@ -9,8 +9,6 @@ imports HOL begin -section {* Abstract orders *} - subsection {* Order syntax *} class ord =