equal
deleted
inserted
replaced
486 Code_Runtime.dynamic_value_strict |
486 Code_Runtime.dynamic_value_strict |
487 (Validator_Batch.get, put_validator_batch, "Exhaustive_Generators.put_validator_batch") |
487 (Validator_Batch.get, put_validator_batch, "Exhaustive_Generators.put_validator_batch") |
488 thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') [] |
488 thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') [] |
489 end; |
489 end; |
490 |
490 |
491 val test_goals = Quickcheck_Common.generator_test_goal_terms compile_generator_expr; |
491 val test_goals = Quickcheck_Common.generator_test_goal_terms ("exhaustive", compile_generator_expr); |
492 |
492 |
493 (* setup *) |
493 (* setup *) |
494 |
494 |
495 val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true); |
495 val active = Attrib.setup_config_bool @{binding quickcheck_exhaustive_active} (K true); |
496 |
496 |