src/HOL/Metis.thy
changeset 62711 09df6a51ad3c
parent 62672 068b430e678f
child 69605 a96320074298
     1.1 --- a/src/HOL/Metis.thy	Sat Mar 26 12:17:02 2016 +0100
     1.2 +++ b/src/HOL/Metis.thy	Sat Mar 26 12:22:15 2016 +0100
     1.3 @@ -10,9 +10,7 @@
     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 = 20]]
    1.10  
    1.11  
    1.12  subsection \<open>Literal selection and lambda-lifting helpers\<close>