src/HOL/Metis.thy
changeset 39980 f175e482dabe
parent 39955 cb9cac7eba29
child 41042 8275f52ac991
equal deleted inserted replaced
39979:b13515940b53 39980:f175e482dabe
    27 by auto
    27 by auto
    28 
    28 
    29 use "Tools/Metis/metis_translate.ML"
    29 use "Tools/Metis/metis_translate.ML"
    30 use "Tools/Metis/metis_reconstruct.ML"
    30 use "Tools/Metis/metis_reconstruct.ML"
    31 use "Tools/Metis/metis_tactics.ML"
    31 use "Tools/Metis/metis_tactics.ML"
    32 setup Metis_Tactics.setup
    32 
       
    33 setup {*
       
    34   Metis_Reconstruct.setup
       
    35   #> Metis_Tactics.setup
       
    36 *}
    33 
    37 
    34 hide_const (open) fequal
    38 hide_const (open) fequal
    35 hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal
    39 hide_fact (open) fequal_def fequal_imp_equal equal_imp_fequal equal_imp_equal
    36 
    40 
    37 end
    41 end