src/HOL/Quickcheck_Narrowing.thy
changeset 46589 689311986778
parent 46308 e5abbec2697a
child 46758 4106258260b3
equal deleted inserted replaced
46588:4895d7f1be42 46589:689311986778
     6 imports Quickcheck_Exhaustive
     6 imports Quickcheck_Exhaustive
     7 uses
     7 uses
     8   ("Tools/Quickcheck/PNF_Narrowing_Engine.hs")
     8   ("Tools/Quickcheck/PNF_Narrowing_Engine.hs")
     9   ("Tools/Quickcheck/Narrowing_Engine.hs")
     9   ("Tools/Quickcheck/Narrowing_Engine.hs")
    10   ("Tools/Quickcheck/narrowing_generators.ML")
    10   ("Tools/Quickcheck/narrowing_generators.ML")
       
    11   ("Tools/Quickcheck/find_unused_assms.ML")
    11 begin
    12 begin
    12 
    13 
    13 subsection {* Counterexample generator *}
    14 subsection {* Counterexample generator *}
    14 
    15 
    15 text {* We create a new target for the necessary code generation setup. *}
    16 text {* We create a new target for the necessary code generation setup. *}
   450      (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Quickcheck_Narrowing.simple_int'') [], Typerep.Typerep (STR ''Int.int'') []])) (partial_term_of (TYPE(simple_int)) t)"
   451      (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Quickcheck_Narrowing.simple_int'') [], Typerep.Typerep (STR ''Int.int'') []])) (partial_term_of (TYPE(simple_int)) t)"
   451 by (rule partial_term_of_anything)
   452 by (rule partial_term_of_anything)
   452 
   453 
   453 *)
   454 *)
   454 
   455 
       
   456 subsection {* The @{text find_unused_assms} command *}
       
   457 
       
   458 use "Tools/Quickcheck/find_unused_assms.ML"
       
   459 
       
   460 subsection {* Closing up *}
       
   461 
   455 hide_type code_int narrowing_type narrowing_term cons property
   462 hide_type code_int narrowing_type narrowing_term cons property
   456 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
   463 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
   457 hide_const (open) Var Ctr "apply" sum cons
   464 hide_const (open) Var Ctr "apply" sum cons
   458 hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def
   465 hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def
   459 
   466 
   460 
   467 end
   461 end