src/HOL/Quickcheck_Exhaustive.thy
changeset 45697 3b7c35a08723
parent 45684 3d6ee9c7d7ef
child 45718 8979b2463fc8
     1.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Wed Nov 30 12:09:29 2011 +0100
     1.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Wed Nov 30 15:07:10 2011 +0100
     1.3 @@ -537,7 +537,9 @@
     1.4  code_const catch_match'
     1.5    (Quickcheck "(_) handle Match => _")
     1.6  
     1.7 -consts unknown :: "'a" ("?")
     1.8 +axiomatization unknown :: 'a
     1.9 +
    1.10 +notation (output) unknown  ("?")
    1.11   
    1.12  use "Tools/Quickcheck/exhaustive_generators.ML"
    1.13  
    1.14 @@ -547,7 +549,7 @@
    1.15  
    1.16  hide_fact orelse_def catch_match_def
    1.17  no_notation orelse (infixr "orelse" 55)
    1.18 -hide_const (open) orelse catch_match mk_map_term check_all_n_lists 
    1.19 +hide_const (open) orelse catch_match catch_match' unknown mk_map_term check_all_n_lists 
    1.20  
    1.21  hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued
    1.22  hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not