author | kleing |
Sun, 06 Apr 2003 21:16:50 +0200 | |
changeset 13901 | af38553e61ee |
parent 7295 | fe09a0c5cebe |
permissions | -rw-r--r-- |
(* Title: HOL/Modelcheck/MuckeExample1.ML ID: $Id$ Author: Olaf Mueller, Jan Philipps, Robert Sandner Copyright 1997 TU Muenchen *) val reach_rws = [INIT_def,N_def,reach_def]; Goal "reach (True,True,True)"; by (simp_tac (Mucke_ss addsimps reach_rws) 1); by (mc_mucke_tac [] 1); qed "reach_ex_thm1"; (*alternative*) Goal "reach (True,True,True)"; by (mc_mucke_tac reach_rws 1); qed "reach_ex_thm1'";