src/HOL/Quickcheck_Narrowing.thy
changeset 43887 442aceb54969
parent 43702 24fb44c1086a
child 45001 5c8d7d6db682
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Mon Jul 18 10:34:21 2011 +0200
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Mon Jul 18 10:34:21 2011 +0200
     1.3 @@ -431,9 +431,8 @@
     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
     1.8 -  C cons conv nonEmpty "apply" sum ensure_testable all exists 
     1.9 -hide_const (open) Var Ctr
    1.10 +hide_const int_of of_int nth error toEnum marker empty C conv nonEmpty ensure_testable all exists 
    1.11 +hide_const (open) Var Ctr "apply" sum cons
    1.12  hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def
    1.13  
    1.14