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