changeset 69815 | 56d5bb8c102e |
parent 69791 | 195aeee8b30a |
child 70749 | 5d06b7bb9d22 |
--- a/src/HOL/Orderings.thy Fri Feb 15 07:11:11 2019 +0000 +++ b/src/HOL/Orderings.thy Fri Feb 15 18:24:22 2019 +0000 @@ -10,7 +10,6 @@ begin ML_file \<open>~~/src/Provers/order.ML\<close> -ML_file \<open>~~/src/Provers/quasi.ML\<close> (* FIXME unused? *) subsection \<open>Abstract ordering\<close>