author wenzelm
Thu, 11 Jun 2009 12:50:20 +0200
changeset 31555 318081898306
parent 31381 b3a785a69538
child 31556 ac0badf13d93
permissions -rw-r--r--
theory Predicate_Compile_ex: enable quick_and_dirty for now, to make it work with internal cheat_tac invocations;

(*  Title:      HOL/ex/ROOT.ML

Miscellaneous examples for Higher-Order Logic.

no_document use_thys [

setmp quick_and_dirty true use_thy "Predicate_Compile_ex";

use_thys [

setmp Proofterm.proofs 2 use_thy "Hilbert_Classical";

use_thy "SVC_Oracle";

fun svc_enabled () = getenv "SVC_HOME" <> "";
fun if_svc_enabled f x = if svc_enabled () then f x else ();

if_svc_enabled use_thy "svc_test";

(* requires a proof-generating SAT solver (zChaff or MiniSAT) to be *)
(* installed:                                                       *)
try use_thy "SAT_Examples";

(* requires zChaff (or some other reasonably fast SAT solver) to be *)
(* installed:                                                       *)
if getenv "ZCHAFF_HOME" <> "" then
  use_thy "Sudoku"
else ();

HTML.with_charset "utf-8" (no_document use_thys)
  ["Hebrew", "Chinese", "Serbian"];