src/HOL/Orderings.thy
changeset 46950 d0181abdbdac
parent 46884 154dc6ec0041
child 46961 5c6955f487e5
equal deleted inserted replaced
46949:94aa7b81bcf6 46950:d0181abdbdac
     4 
     4 
     5 header {* Abstract orderings *}
     5 header {* Abstract orderings *}
     6 
     6 
     7 theory Orderings
     7 theory Orderings
     8 imports HOL
     8 imports HOL
       
     9 keywords "print_orders" :: diag
     9 uses
    10 uses
    10   "~~/src/Provers/order.ML"
    11   "~~/src/Provers/order.ML"
    11   "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
    12   "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
    12 begin
    13 begin
    13 
    14