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