src/HOL/ex/Quickcheck_Examples.thy
changeset 16417 9bc16273c2d4
parent 14592 dd1a2905ea73
child 17388 495c799df31d
     1.1 --- a/src/HOL/ex/Quickcheck_Examples.thy	Fri Jun 17 11:35:35 2005 +0200
     1.2 +++ b/src/HOL/ex/Quickcheck_Examples.thy	Fri Jun 17 16:12:49 2005 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  header {* Examples for the 'quickcheck' command *}
     1.6  
     1.7 -theory Quickcheck_Examples = Main:
     1.8 +theory Quickcheck_Examples imports Main begin
     1.9  
    1.10  text {*
    1.11  The 'quickcheck' command allows to find counterexamples by evaluating