| changeset 62711 | 09df6a51ad3c |
| parent 62672 | 068b430e678f |
| child 69605 | a96320074298 |
--- a/src/HOL/Metis.thy Sat Mar 26 12:17:02 2016 +0100 +++ b/src/HOL/Metis.thy Sat Mar 26 12:22:15 2016 +0100 @@ -10,9 +10,7 @@ imports ATP begin -declare [[ML_print_depth = 0]] ML_file "~~/src/Tools/Metis/metis.ML" -declare [[ML_print_depth = 20]] subsection \<open>Literal selection and lambda-lifting helpers\<close>