src/HOL/Modelcheck/Example.ML
author mueller
Fri, 16 May 1997 16:10:19 +0200
changeset 3219 9854e3ea09e7
parent 3210 e80db1660614
child 3225 cee363fc07d7
permissions -rw-r--r--
commented out qed (in case the MC is unavailable);

(*  Title:      HOL/Modelcheck/Example.ML
    ID:         $Id$
    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
    Copyright   1997  TU Muenchen
*)

val reach_rws = [reach_def,INIT_def,N_def];


goal thy "reach (True,True,True)";
by (simp_tac (MC_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*)
by (mc_tac 1);

(*qed "reach_ex_thm1";*)