changeset 43314 | a9090cabca14 |
parent 43312 | 7a31f9064f99 |
child 43315 | 893de45ac28d |
--- a/src/HOL/Quickcheck_Narrowing.thy Thu Jun 09 08:32:18 2011 +0200 +++ b/src/HOL/Quickcheck_Narrowing.thy Thu Jun 09 08:32:19 2011 +0200 @@ -533,5 +533,6 @@ hide_type (open) code_int narrowing_type narrowing_term cons hide_const (open) int_of of_int nth error toEnum map_index split_At empty C cons conv nonEmpty "apply" sum cons1 cons2 ensure_testable all exists +hide_fact empty_def end \ No newline at end of file