src/HOL/Quickcheck_Narrowing.thy
changeset 46589 689311986778
parent 46308 e5abbec2697a
child 46758 4106258260b3
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Wed Feb 22 12:30:01 2012 +0100
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Wed Feb 22 17:22:53 2012 +0100
     1.3 @@ -8,6 +8,7 @@
     1.4    ("Tools/Quickcheck/PNF_Narrowing_Engine.hs")
     1.5    ("Tools/Quickcheck/Narrowing_Engine.hs")
     1.6    ("Tools/Quickcheck/narrowing_generators.ML")
     1.7 +  ("Tools/Quickcheck/find_unused_assms.ML")
     1.8  begin
     1.9  
    1.10  subsection {* Counterexample generator *}
    1.11 @@ -452,10 +453,15 @@
    1.12  
    1.13  *)
    1.14  
    1.15 +subsection {* The @{text find_unused_assms} command *}
    1.16 +
    1.17 +use "Tools/Quickcheck/find_unused_assms.ML"
    1.18 +
    1.19 +subsection {* Closing up *}
    1.20 +
    1.21  hide_type code_int narrowing_type narrowing_term cons property
    1.22  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.23  hide_const (open) Var Ctr "apply" sum cons
    1.24  hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def
    1.25  
    1.26 -
    1.27  end