src/HOL/Metis.thy
changeset 62672 068b430e678f
parent 60758 d8d85a8172b5
child 62711 09df6a51ad3c
equal deleted inserted replaced
62671:a9ee1f240b81 62672:068b430e678f
    10 imports ATP
    10 imports ATP
    11 begin
    11 begin
    12 
    12 
    13 declare [[ML_print_depth = 0]]
    13 declare [[ML_print_depth = 0]]
    14 ML_file "~~/src/Tools/Metis/metis.ML"
    14 ML_file "~~/src/Tools/Metis/metis.ML"
    15 declare [[ML_print_depth = 10]]
    15 declare [[ML_print_depth = 20]]
    16 
    16 
    17 
    17 
    18 subsection \<open>Literal selection and lambda-lifting helpers\<close>
    18 subsection \<open>Literal selection and lambda-lifting helpers\<close>
    19 
    19 
    20 definition select :: "'a \<Rightarrow> 'a" where
    20 definition select :: "'a \<Rightarrow> 'a" where