equal
deleted
inserted
replaced
531 |
531 |
532 setup {* Exhaustive_Generators.setup *} |
532 setup {* Exhaustive_Generators.setup *} |
533 |
533 |
534 declare [[quickcheck_batch_tester = exhaustive]] |
534 declare [[quickcheck_batch_tester = exhaustive]] |
535 |
535 |
536 hide_fact orelse_def catch_match_def |
536 hide_fact orelse_def |
537 no_notation orelse (infixr "orelse" 55) |
537 no_notation orelse (infixr "orelse" 55) |
538 hide_const (open) orelse catch_match catch_match' unknown mk_map_term check_all_n_lists |
538 hide_const (open) orelse unknown mk_map_term check_all_n_lists |
539 |
539 |
540 hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued |
540 hide_type (open) cps pos_bound_cps neg_bound_cps unknown three_valued |
541 hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not |
541 hide_const (open) cps_empty cps_single cps_bind cps_plus cps_if cps_not |
542 pos_bound_cps_empty pos_bound_cps_single pos_bound_cps_bind pos_bound_cps_plus pos_bound_cps_if pos_bound_cps_not |
542 pos_bound_cps_empty pos_bound_cps_single pos_bound_cps_bind pos_bound_cps_plus pos_bound_cps_if pos_bound_cps_not |
543 neg_bound_cps_empty neg_bound_cps_single neg_bound_cps_bind neg_bound_cps_plus neg_bound_cps_if neg_bound_cps_not |
543 neg_bound_cps_empty neg_bound_cps_single neg_bound_cps_bind neg_bound_cps_plus neg_bound_cps_if neg_bound_cps_not |