src/HOL/Metis.thy
changeset 56946 10d9bd4ea94f
parent 56281 03c3d1a7c3b8
child 58818 ee85e7b82d00
     1.1 --- a/src/HOL/Metis.thy	Tue May 13 11:10:22 2014 +0200
     1.2 +++ b/src/HOL/Metis.thy	Tue May 13 11:10:23 2014 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4  ML_file "~~/src/Tools/Metis/metis.ML"
     1.5  declare [[ML_print_depth = 10]]
     1.6  
     1.7 +
     1.8  subsection {* Literal selection and lambda-lifting helpers *}
     1.9  
    1.10  definition select :: "'a \<Rightarrow> 'a" where
    1.11 @@ -45,12 +46,11 @@
    1.12  
    1.13  setup {* Metis_Tactic.setup *}
    1.14  
    1.15 -hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fequal
    1.16 -    lambda
    1.17 -hide_fact (open) select_def not_atomize atomize_not_select not_atomize_select
    1.18 -    select_FalseI fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
    1.19 -    fequal_def fTrue_ne_fFalse fNot_table fconj_table fdisj_table fimplies_table
    1.20 -    fequal_table fAll_table fEx_table fNot_law fComp_law fconj_laws fdisj_laws
    1.21 -    fimplies_laws fequal_laws fAll_law fEx_law lambda_def eq_lambdaI
    1.22 +hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fAll fEx fequal lambda
    1.23 +hide_fact (open) select_def not_atomize atomize_not_select not_atomize_select select_FalseI
    1.24 +  fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def fAll_def fEx_def fequal_def
    1.25 +  fTrue_ne_fFalse fNot_table fconj_table fdisj_table fimplies_table fAll_table fEx_table
    1.26 +  fequal_table fAll_table fEx_table fNot_law fComp_law fconj_laws fdisj_laws fimplies_laws
    1.27 +  fequal_laws fAll_law fEx_law lambda_def eq_lambdaI
    1.28  
    1.29  end