Added new functions to handle HOL goals and lemmas.
Added a funtion to send types and sorts information to ATP: they are clauses written to a separate file.
Removed several functions definitions, and combined them with those in other files.
(* Title: HOL/Modelcheck/ROOT.ML
ID: $Id$
Author: Olaf Mueller and Tobias Hamberger and Robert Sandner, TU Muenchen
Basic Modelchecker examples.
*)
time_use_thy "CTL";
(* Einhoven model checker *)
time_use_thy "EindhovenSyn";
if_eindhoven_enabled time_use_thy "EindhovenExample";
(* Mucke -- mu-calculus model checker from Karlsruhe *)
time_use "mucke_oracle.ML";
time_use_thy "MuckeSyn";
if_mucke_enabled time_use_thy "MuckeExample1";
if_mucke_enabled time_use_thy "MuckeExample2";