src/HOL/ex/Quickcheck_Narrowing_Examples.thy
changeset 43318 825f4f0dcf71
parent 43239 42f82fda796b
child 43356 2dee03f192b7
equal deleted inserted replaced
43317:f9283eb3a4bf 43318:825f4f0dcf71
     4 *)
     4 *)
     5 
     5 
     6 header {* Examples for narrowing-based testing  *}
     6 header {* Examples for narrowing-based testing  *}
     7 
     7 
     8 theory Quickcheck_Narrowing_Examples
     8 theory Quickcheck_Narrowing_Examples
     9 imports "~~/src/HOL/Library/Quickcheck_Narrowing"
     9 imports Main
    10 begin
    10 begin
    11 
    11 
    12 subsection {* Minimalistic examples *}
    12 subsection {* Minimalistic examples *}
    13 (*
    13 (*
    14 lemma
    14 lemma