the simple exhaustive compilation also indicates if counterexample is potentially spurious;
(* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *)
no_document use_thys ["../Number_Theory/Primes"];
use_thys [
"Basic_Logic",
"Cantor",
"Peirce",
"Drinker",
"Expr_Compiler",
"Group",
"Summation",
"Knaster_Tarski",
"Mutilated_Checkerboard",
"Puzzle",
"Nested_Datatype",
"Hoare_Ex"
];