(* Title: HOL/Modelcheck/EindhovenExample.ML
ID: $Id$
Author: Olaf Mueller, Jan Philipps, Robert Sandner
Copyright 1997 TU Muenchen
*)
val reach_rws = [reach_def,INIT_def,N_def];
Goal "reach (True,True,True)";
by (simp_tac (Eindhoven_ss addsimps reach_rws) 1);
(*show the current proof state using the model checker syntax*)
setmp print_mode ["Eindhoven"] pr ();
(* actually invoke the model checker *)
(* try out after installing the model checker: see the README file *)
(* by (mc_eindhoven_tac 1); *)
(*qed "reach_ex_thm";*)
(* just to make a proof in this file :-) *)
Goalw [INIT_def] "INIT (a,b,c) = (~a & ~b &~c)";
by (Simp_tac 1);
qed"init_state";