src/HOL/Nunchaku/Nunchaku.thy
changeset 64389 6273d4c8325b
child 64407 5c5b9d945625
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Nunchaku/Nunchaku.thy	Mon Oct 24 22:42:07 2016 +0200
     1.3 @@ -0,0 +1,41 @@
     1.4 +(*  Title:      HOL/Nunchaku/Nunchaku.thy
     1.5 +    Author:     Jasmin Blanchette, Inria Nancy, LORIA, MPII
     1.6 +    Copyright   2015, 2016
     1.7 +
     1.8 +Nunchaku: Yet another counterexample generator for Isabelle/HOL.
     1.9 +
    1.10 +Nunchaku relies on an external program of the same name. The program is still
    1.11 +being actively developed. The sources are available at
    1.12 +
    1.13 +    https://github.com/nunchaku-inria
    1.14 +*)
    1.15 +
    1.16 +theory Nunchaku
    1.17 +imports Main
    1.18 +keywords
    1.19 +  "nunchaku" :: diag and
    1.20 +  "nunchaku_params" :: thy_decl
    1.21 +begin
    1.22 +
    1.23 +consts unreachable :: 'a
    1.24 +
    1.25 +definition The_unsafe :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" where
    1.26 +  "The_unsafe = The"
    1.27 +
    1.28 +definition rmember :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" where
    1.29 +  "rmember A x \<longleftrightarrow> x \<in> A"
    1.30 +
    1.31 +ML_file "Tools/nunchaku_util.ML"
    1.32 +ML_file "Tools/nunchaku_collect.ML"
    1.33 +ML_file "Tools/nunchaku_problem.ML"
    1.34 +ML_file "Tools/nunchaku_translate.ML"
    1.35 +ML_file "Tools/nunchaku_model.ML"
    1.36 +ML_file "Tools/nunchaku_reconstruct.ML"
    1.37 +ML_file "Tools/nunchaku_display.ML"
    1.38 +ML_file "Tools/nunchaku_tool.ML"
    1.39 +ML_file "Tools/nunchaku.ML"
    1.40 +ML_file "Tools/nunchaku_commands.ML"
    1.41 +
    1.42 +hide_const (open) unreachable The_unsafe rmember
    1.43 +
    1.44 +end