equal
deleted
inserted
replaced
2 |
2 |
3 header {* A simple counterexample generator performing random testing *} |
3 header {* A simple counterexample generator performing random testing *} |
4 |
4 |
5 theory Quickcheck |
5 theory Quickcheck |
6 imports Random Code_Evaluation Enum |
6 imports Random Code_Evaluation Enum |
7 uses ("Tools/Quickcheck/random_generators.ML") |
7 uses |
|
8 "Tools/Quickcheck/quickcheck_common.ML" |
|
9 ("Tools/Quickcheck/random_generators.ML") |
8 begin |
10 begin |
9 |
11 |
10 notation fcomp (infixl "\<circ>>" 60) |
12 notation fcomp (infixl "\<circ>>" 60) |
11 notation scomp (infixl "\<circ>\<rightarrow>" 60) |
13 notation scomp (infixl "\<circ>\<rightarrow>" 60) |
12 |
14 |