| changeset 56281 | 03c3d1a7c3b8 |
| parent 55509 | bd67ebe275e0 |
| child 56946 | 10d9bd4ea94f |
--- a/src/HOL/Metis.thy Tue Mar 25 17:59:34 2014 +0100 +++ b/src/HOL/Metis.thy Tue Mar 25 19:03:02 2014 +0100 @@ -10,7 +10,9 @@ imports ATP begin +declare [[ML_print_depth = 0]] ML_file "~~/src/Tools/Metis/metis.ML" +declare [[ML_print_depth = 10]] subsection {* Literal selection and lambda-lifting helpers *}