Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Modelcheck/Example.ML
author wenzelm
Tue, 20 May 1997 19:29:50 +0200
changeset 3257 4e3724e0659f
parent 3225 cee363fc07d7
child 3380 2986e3b1f86a
permissions -rw-r--r--
README generation;

(*  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 *)
(* try out after installing the model checker: see the README file *)

(* by (mc_tac 1); *)

(*qed "reach_ex_thm1";*)
isabelle