equal
deleted
inserted
replaced
1 (* Title: HOL/Mutabelle/mutabelle_extra.ML |
1 (* Title: HOL/Mutabelle/mutabelle_extra.ML |
2 Author: Stefan Berghofer, Jasmin Blanchette, Lukas Bulwahn, TU Muenchen |
2 Author: Stefan Berghofer, Jasmin Blanchette, Lukas Bulwahn, TU Muenchen |
3 |
3 |
4 Invokation of Counterexample generators |
4 Invokation of Counterexample generators. |
5 *) |
5 *) |
|
6 |
6 signature MUTABELLE_EXTRA = |
7 signature MUTABELLE_EXTRA = |
7 sig |
8 sig |
8 |
9 |
9 val take_random : int -> 'a list -> 'a list |
10 val take_random : int -> 'a list -> 'a list |
10 |
11 |