hiding internal constants and facts more properly
authorbulwahn
Thu Dec 01 22:16:26 2011 +0100 (2011-12-01)
changeset 457336bb30ae1abfe
parent 45732 ac5775bbc748
child 45734 1024dd30da42
hiding internal constants and facts more properly
src/HOL/Quickcheck.thy
src/HOL/Quickcheck_Exhaustive.thy
     1.1 --- a/src/HOL/Quickcheck.thy	Thu Dec 01 22:16:23 2011 +0100
     1.2 +++ b/src/HOL/Quickcheck.thy	Thu Dec 01 22:16:26 2011 +0100
     1.3 @@ -157,6 +157,9 @@
     1.4  no_notation fcomp (infixl "\<circ>>" 60)
     1.5  no_notation scomp (infixl "\<circ>\<rightarrow>" 60)
     1.6  
     1.7 +hide_fact catch_match_def
     1.8 +hide_const (open) catch_match
     1.9 +
    1.10  subsection {* The Random-Predicate Monad *} 
    1.11  
    1.12  fun iter' ::
     2.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Thu Dec 01 22:16:23 2011 +0100
     2.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Thu Dec 01 22:16:26 2011 +0100
     2.3 @@ -533,9 +533,9 @@
     2.4  
     2.5  declare [[quickcheck_batch_tester = exhaustive]]
     2.6  
     2.7 -hide_fact orelse_def catch_match_def
     2.8 +hide_fact orelse_def
     2.9  no_notation orelse (infixr "orelse" 55)
    2.10 -hide_const (open) orelse catch_match catch_match' unknown mk_map_term check_all_n_lists 
    2.11 +hide_const (open) orelse unknown mk_map_term check_all_n_lists 
    2.12  
    2.13  hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued
    2.14  hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not