src/HOL/Orderings.thy
changeset 48891 c0eafbd55de3
parent 47432 e1576d13e933
child 49660 de49d9b4d7bc
     1.1 --- a/src/HOL/Orderings.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -7,11 +7,11 @@
     1.4  theory Orderings
     1.5  imports HOL
     1.6  keywords "print_orders" :: diag
     1.7 -uses
     1.8 -  "~~/src/Provers/order.ML"
     1.9 -  "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
    1.10  begin
    1.11  
    1.12 +ML_file "~~/src/Provers/order.ML"
    1.13 +ML_file "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
    1.14 +
    1.15  subsection {* Syntactic orders *}
    1.16  
    1.17  class ord =