equal
deleted
inserted
replaced
346 primrec eval_cfun :: "'b cfun => 'a => 'b" |
346 primrec eval_cfun :: "'b cfun => 'a => 'b" |
347 where |
347 where |
348 "eval_cfun (Constant c) y = c" |
348 "eval_cfun (Constant c) y = c" |
349 |
349 |
350 hide_type (open) cfun |
350 hide_type (open) cfun |
351 hide_const (open) Constant eval_cfun |
351 hide_const (open) Constant eval_cfun Abs_cfun Rep_cfun |
352 |
352 |
353 subsubsection {* Setting up the counterexample generator *} |
353 subsubsection {* Setting up the counterexample generator *} |
354 |
354 |
355 use "Tools/Quickcheck/narrowing_generators.ML" |
355 use "Tools/Quickcheck/narrowing_generators.ML" |
356 |
356 |