src/HOL/Nitpick_Examples/Tests_Nits.thy
author blanchet
Tue Jun 22 12:19:06 2010 +0200 (2010-06-22)
changeset 37495 650fae5eea93
parent 35076 cc19e2aef17e
child 45035 60d2c03d5c70
permissions -rw-r--r--
make the Nitpick_Example theory processable even when Kodkodi is not installed;
so that at least the "theory" aspects of it (as opposed to the diagnosis offered by Nitpick) are checked on everybody's machines
blanchet@33197
     1
(*  Title:      HOL/Nitpick_Examples/Tests_Nits.thy
blanchet@33197
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@35076
     3
    Copyright   2009, 2010
blanchet@33197
     4
blanchet@33197
     5
Nitpick tests.
blanchet@33197
     6
*)
blanchet@33197
     7
blanchet@33197
     8
header {* Nitpick Tests *}
blanchet@33197
     9
blanchet@33197
    10
theory Tests_Nits
blanchet@33197
    11
imports Main
blanchet@33197
    12
begin
blanchet@33197
    13
blanchet@37495
    14
ML {* () |> getenv "KODKODI" <> "" ? Nitpick_Tests.run_all_tests *}
blanchet@33197
    15
blanchet@33197
    16
end