equal
deleted
inserted
replaced
1 (* Title: HOL/Modelcheck/MuckeExample2.ML |
|
2 ID: $Id$ |
|
3 Author: Olaf Mueller, Jan Philipps, Robert Sandner |
|
4 Copyright 1997 TU Muenchen |
|
5 *) |
|
6 |
|
7 |
|
8 (* prints the mucke output on the screen *) |
|
9 (* trace_mc := true; *) |
|
10 val Reach_rws = [Init_def,R_def,Reach_def,Reach2_def]; |
|
11 |
|
12 Goal "Reach2 True"; |
|
13 by (simp_tac (Mucke_ss addsimps Reach_rws) 1); |
|
14 by (mc_mucke_tac [] 1); |
|
15 qed "Reach_thm"; |
|
16 |
|
17 (*alternative:*) |
|
18 goal thy "Reach2 True"; |
|
19 by (mc_mucke_tac Reach_rws 1); |
|
20 qed "Reach_thm'"; |
|