src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
changeset 58889 5b7a9633cfa8
parent 58813 625d04d4fd2a
child 61169 4de9ff3ea29a
equal deleted inserted replaced
58888:9537bf1c4853 58889:5b7a9633cfa8
     1 (*  Title:      HOL/Quickcheck_Examples/Quickcheck_Examples.thy
     1 (*  Title:      HOL/Quickcheck_Examples/Quickcheck_Examples.thy
     2     Author:     Stefan Berghofer, Lukas Bulwahn
     2     Author:     Stefan Berghofer, Lukas Bulwahn
     3     Copyright   2004 - 2010 TU Muenchen
     3     Copyright   2004 - 2010 TU Muenchen
     4 *)
     4 *)
     5 
     5 
     6 header {* Examples for the 'quickcheck' command *}
     6 section {* Examples for the 'quickcheck' command *}
     7 
     7 
     8 theory Quickcheck_Examples
     8 theory Quickcheck_Examples
     9 imports Complex_Main "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/DAList_Multiset"
     9 imports Complex_Main "~~/src/HOL/Library/Dlist" "~~/src/HOL/Library/DAList_Multiset"
    10 begin
    10 begin
    11 
    11