author | mueller |
Thu, 22 Apr 1999 10:56:37 +0200 | |
changeset 6466 | 2eba94dc5951 |
child 7295 | fe09a0c5cebe |
permissions | -rw-r--r-- |
(* Title: HOL/Modelcheck/MuckeExample2.ML ID: $Id$ Author: Olaf Mueller, Jan Philipps, Robert Sandner Copyright 1997 TU Muenchen *) (* prints the mucke output on the screen *) (* trace_mc := true; *) val Reach_rws = [Init_def,R_def,Reach_def,Reach2_def]; (* goal thy "Reach2 True"; by (simp_tac (Mucke_ss addsimps Reach_rws) 1); by (mc_mucke_tac thy [] 1); qed "Reach_thm"; (* Alternative: *) goal thy "Reach2 True"; by (mc_mucke_tac thy Reach_rws 1); qed "Reach_thm"; *)