src/HOL/Quickcheck_Narrowing.thy
changeset 58889 5b7a9633cfa8
parent 58826 2ed2eaabe3df
child 59104 a14475f044b2
equal deleted inserted replaced
58888:9537bf1c4853 58889:5b7a9633cfa8
     1 (* Author: Lukas Bulwahn, TU Muenchen *)
     1 (* Author: Lukas Bulwahn, TU Muenchen *)
     2 
     2 
     3 header {* Counterexample generator performing narrowing-based testing *}
     3 section {* Counterexample generator performing narrowing-based testing *}
     4 
     4 
     5 theory Quickcheck_Narrowing
     5 theory Quickcheck_Narrowing
     6 imports Quickcheck_Random
     6 imports Quickcheck_Random
     7 keywords "find_unused_assms" :: diag
     7 keywords "find_unused_assms" :: diag
     8 begin
     8 begin