src/HOL/Metis.thy
changeset 58818 ee85e7b82d00
parent 56946 10d9bd4ea94f
child 58889 5b7a9633cfa8
equal deleted inserted replaced
58817:4cd778c91fdc 58818:ee85e7b82d00
    42 
    42 
    43 ML_file "Tools/Metis/metis_generate.ML"
    43 ML_file "Tools/Metis/metis_generate.ML"
    44 ML_file "Tools/Metis/metis_reconstruct.ML"
    44 ML_file "Tools/Metis/metis_reconstruct.ML"
    45 ML_file "Tools/Metis/metis_tactic.ML"
    45 ML_file "Tools/Metis/metis_tactic.ML"
    46 
    46 
    47 setup {* Metis_Tactic.setup *}
       
    48 
       
    49 hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fAll fEx fequal lambda
    47 hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fAll fEx fequal lambda
    50 hide_fact (open) select_def not_atomize atomize_not_select not_atomize_select select_FalseI
    48 hide_fact (open) select_def not_atomize atomize_not_select not_atomize_select select_FalseI
    51   fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def fAll_def fEx_def fequal_def
    49   fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def fAll_def fEx_def fequal_def
    52   fTrue_ne_fFalse fNot_table fconj_table fdisj_table fimplies_table fAll_table fEx_table
    50   fTrue_ne_fFalse fNot_table fconj_table fdisj_table fimplies_table fAll_table fEx_table
    53   fequal_table fAll_table fEx_table fNot_law fComp_law fconj_laws fdisj_laws fimplies_laws
    51   fequal_table fAll_table fEx_table fNot_law fComp_law fconj_laws fdisj_laws fimplies_laws