src/HOL/Orderings.thy
changeset 22886 cdff6ef76009
parent 22841 83b9f2d3fb3c
child 22916 8caf6da610e2
     1.1 --- a/src/HOL/Orderings.thy	Wed May 09 07:53:04 2007 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Wed May 09 07:53:06 2007 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Syntactic and abstract orders *}
     1.5  
     1.6  theory Orderings
     1.7 -imports HOL
     1.8 +imports Code_Generator
     1.9  begin
    1.10  
    1.11  subsection {* Order syntax *}
    1.12 @@ -798,7 +798,7 @@
    1.13  
    1.14  subsection {* Order on bool *}
    1.15  
    1.16 -instance bool :: linorder 
    1.17 +instance bool :: order 
    1.18    le_bool_def: "P \<le> Q \<equiv> P \<longrightarrow> Q"
    1.19    less_bool_def: "P < Q \<equiv> P \<le> Q \<and> P \<noteq> Q"
    1.20    by default (auto simp add: le_bool_def less_bool_def)
    1.21 @@ -892,11 +892,6 @@
    1.22  
    1.23  ML {*
    1.24  val monoI = @{thm monoI};
    1.25 -
    1.26 -structure HOL =
    1.27 -struct
    1.28 -  val thy = theory "HOL";
    1.29 -end;
    1.30 -*}  -- "belongs to theory HOL"
    1.31 +*}
    1.32  
    1.33  end