src/Tools/Auto_Counterexample.thy
author bulwahn
Thu, 12 Nov 2009 20:38:57 +0100
changeset 33649 854173fcd21c
parent 33561 ab01b72715ef
permissions -rw-r--r--
added a tabled implementation of the reflexive transitive closure
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