changeset 69605 | a96320074298 |
parent 69597 | ff784d5a5bfb |
child 69791 | 195aeee8b30a |
--- a/src/HOL/Orderings.thy Sun Jan 06 13:44:33 2019 +0100 +++ b/src/HOL/Orderings.thy Sun Jan 06 15:04:34 2019 +0100 @@ -9,8 +9,8 @@ keywords "print_orders" :: diag begin -ML_file "~~/src/Provers/order.ML" -ML_file "~~/src/Provers/quasi.ML" (* FIXME unused? *) +ML_file \<open>~~/src/Provers/order.ML\<close> +ML_file \<open>~~/src/Provers/quasi.ML\<close> (* FIXME unused? *) subsection \<open>Abstract ordering\<close>