src/HOL/OrderedGroup.thy
changeset 21328 73bb86d0f483
parent 21312 1d39091a3208
child 21382 d71aed9286d3
     1.1 --- a/src/HOL/OrderedGroup.thy	Mon Nov 13 15:43:04 2006 +0100
     1.2 +++ b/src/HOL/OrderedGroup.thy	Mon Nov 13 15:43:05 2006 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* Ordered Groups *}
     1.5  
     1.6  theory OrderedGroup
     1.7 -imports Inductive LOrder
     1.8 +imports Set LOrder
     1.9  uses "~~/src/Provers/Arith/abel_cancel.ML"
    1.10  begin
    1.11