src/HOL/Metis.thy
changeset 47946 33afcfad3f8d
parent 46950 d0181abdbdac
child 48891 c0eafbd55de3
     1.1 --- a/src/HOL/Metis.thy	Mon May 21 10:39:31 2012 +0200
     1.2 +++ b/src/HOL/Metis.thy	Mon May 21 10:39:32 2012 +0200
     1.3 @@ -47,10 +47,13 @@
     1.4  
     1.5  setup {* Metis_Tactic.setup *}
     1.6  
     1.7 -hide_const (open) fFalse fTrue fNot fconj fdisj fimplies fequal select lambda
     1.8 -hide_fact (open) fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
     1.9 -    fequal_def select_def not_atomize atomize_not_select not_atomize_select
    1.10 -    select_FalseI lambda_def eq_lambdaI
    1.11 +hide_const (open) select fFalse fTrue fNot fComp fconj fdisj fimplies fequal
    1.12 +    lambda
    1.13 +hide_fact (open) select_def not_atomize atomize_not_select not_atomize_select
    1.14 +    select_FalseI fFalse_def fTrue_def fNot_def fconj_def fdisj_def fimplies_def
    1.15 +    fequal_def fTrue_ne_fFalse fNot_table fconj_table fdisj_table fimplies_table
    1.16 +    fequal_table fAll_table fEx_table fNot_law fComp_law fconj_laws fdisj_laws
    1.17 +    fimplies_laws fequal_laws fAll_law fEx_law lambda_def eq_lambdaI
    1.18  
    1.19  
    1.20  subsection {* Try0 *}