src/HOL/Metis.thy
changeset 56946 10d9bd4ea94f
parent 56281 03c3d1a7c3b8
child 58818 ee85e7b82d00
equal deleted inserted replaced
56945:3d1ead21a055 56946:10d9bd4ea94f
    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 = 10]]
       
    16 
    16 
    17 
    17 subsection {* Literal selection and lambda-lifting helpers *}
    18 subsection {* Literal selection and lambda-lifting helpers *}
    18 
    19 
    19 definition select :: "'a \<Rightarrow> 'a" where
    20 definition select :: "'a \<Rightarrow> 'a" where
    20 "select = (\<lambda>x. x)"
    21 "select = (\<lambda>x. x)"
    43 ML_file "Tools/Metis/metis_reconstruct.ML"
    44 ML_file "Tools/Metis/metis_reconstruct.ML"
    44 ML_file "Tools/Metis/metis_tactic.ML"
    45 ML_file "Tools/Metis/metis_tactic.ML"
    45 
    46 
    46 setup {* Metis_Tactic.setup *}
    47 setup {* Metis_Tactic.setup *}
    47 
    48 
    48 hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fequal
    49 hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fAll fEx fequal lambda
    49     lambda
    50 hide_fact (open) select_def not_atomize atomize_not_select not_atomize_select select_FalseI
    50 hide_fact (open) select_def not_atomize atomize_not_select not_atomize_select
    51   fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def fAll_def fEx_def fequal_def
    51     select_FalseI fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
    52   fTrue_ne_fFalse fNot_table fconj_table fdisj_table fimplies_table fAll_table fEx_table
    52     fequal_def fTrue_ne_fFalse fNot_table fconj_table fdisj_table fimplies_table
    53   fequal_table fAll_table fEx_table fNot_law fComp_law fconj_laws fdisj_laws fimplies_laws
    53     fequal_table fAll_table fEx_table fNot_law fComp_law fconj_laws fdisj_laws
    54   fequal_laws fAll_law fEx_law lambda_def eq_lambdaI
    54     fimplies_laws fequal_laws fAll_law fEx_law lambda_def eq_lambdaI
       
    55 
    55 
    56 end
    56 end