| changeset 48891 | c0eafbd55de3 |
| parent 47432 | e1576d13e933 |
| child 49660 | de49d9b4d7bc |
--- a/src/HOL/Orderings.thy Wed Aug 22 22:47:16 2012 +0200 +++ b/src/HOL/Orderings.thy Wed Aug 22 22:55:41 2012 +0200 @@ -7,11 +7,11 @@ theory Orderings imports HOL keywords "print_orders" :: diag -uses - "~~/src/Provers/order.ML" - "~~/src/Provers/quasi.ML" (* FIXME unused? *) begin +ML_file "~~/src/Provers/order.ML" +ML_file "~~/src/Provers/quasi.ML" (* FIXME unused? *) + subsection {* Syntactic orders *} class ord =