src/Tools/Auto_Counterexample.thy
author bulwahn
Thu, 12 Nov 2009 09:10:22 +0100
changeset 33620 b6bf2dc5aed7
parent 33561 ab01b72715ef
permissions -rw-r--r--
added interface of user proposals for names of generated constants
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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