src/HOL/Library/Quickcheck_Narrowing.thy
changeset 41962 27a61a3266d8
parent 41961 fdd37cfcd4a3
child 41964 13904699c859
equal deleted inserted replaced
41961:fdd37cfcd4a3 41962:27a61a3266d8
     2 
     2 
     3 header {* Counterexample generator preforming narrowing-based testing *}
     3 header {* Counterexample generator preforming narrowing-based testing *}
     4 
     4 
     5 theory Quickcheck_Narrowing
     5 theory Quickcheck_Narrowing
     6 imports Main "~~/src/HOL/Library/Code_Char"
     6 imports Main "~~/src/HOL/Library/Code_Char"
     7 uses ("~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML")
     7 uses
       
     8   ("~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML")
     8 begin
     9 begin
     9 
    10 
    10 subsection {* Counterexample generator *}
    11 subsection {* Counterexample generator *}
    11 
    12 
    12 subsubsection {* Code generation setup *}
    13 subsubsection {* Code generation setup *}