src/HOL/Orderings.thy
changeset 23247 b99dce43d252
parent 23212 82881b1ae9c6
child 23263 0c227412b285
--- a/src/HOL/Orderings.thy	Tue Jun 05 12:12:25 2007 +0200
+++ b/src/HOL/Orderings.thy	Tue Jun 05 15:16:08 2007 +0200
@@ -6,7 +6,7 @@
 header {* Syntactic and abstract orders *}
 
 theory Orderings
-imports Code_Generator
+imports HOL
 begin
 
 subsection {* Order syntax *}