src/HOL/Quickcheck_Narrowing.thy
changeset 45818 53a697f5454a
parent 45734 1024dd30da42
child 46032 0da934e135b0
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Mon Dec 12 12:03:34 2011 +0100
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Mon Dec 12 13:45:54 2011 +0100
     1.3 @@ -448,7 +448,7 @@
     1.4  *)
     1.5  
     1.6  hide_type code_int narrowing_type narrowing_term cons property
     1.7 -hide_const int_of of_int nth error toEnum marker empty C conv nonEmpty ensure_testable all exists 
     1.8 +hide_const int_of of_int nat_of map_cons nth error toEnum marker empty C conv nonEmpty ensure_testable all exists drawn_from around_zero
     1.9  hide_const (open) Var Ctr "apply" sum cons
    1.10  hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def
    1.11