| author | nipkow |
| Fri, 13 Nov 2009 22:01:20 +0100 | |
| changeset 33677 | ade8e136efb4 |
| parent 33561 | ab01b72715ef |
| permissions | -rw-r--r-- |
|
33561
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset
|
1 |
(* Title: Tools/Auto_Counterexample.thy |
|
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset
|
2 |
Author: Jasmin Blanchette, TU Muenchen |
|
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset
|
3 |
|
|
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset
|
4 |
Counterexample Search Unit (do not abbreviate!). |
|
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset
|
5 |
*) |
|
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset
|
6 |
|
|
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset
|
7 |
header {* Counterexample Search Unit *}
|
|
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset
|
8 |
|
|
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset
|
9 |
theory Auto_Counterexample |
|
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset
|
10 |
imports Pure |
|
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset
|
11 |
uses |
|
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset
|
12 |
"~~/src/Tools/auto_counterexample.ML" |
|
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset
|
13 |
begin |
|
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset
|
14 |
|
|
ab01b72715ef
introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet
parents:
diff
changeset
|
15 |
end |