equal
deleted
inserted
replaced
|
1 (* Title: HOL/Modelcheck/MuckeExample1.ML |
|
2 ID: $Id$ |
|
3 Author: Olaf Mueller, Jan Philipps, Robert Sandner |
|
4 Copyright 1997 TU Muenchen |
|
5 *) |
|
6 |
|
7 val reach_rws = [INIT_def,N_def,reach_def]; |
|
8 |
|
9 (* |
|
10 goal thy "reach (True,True,True)"; |
|
11 by (simp_tac (Mucke_ss addsimps reach_rws) 1); |
|
12 by (mc_mucke_tac thy [] 1); |
|
13 qed "reach_ex_thm1"; |
|
14 |
|
15 (* Alternative: *) |
|
16 goal thy "reach (True,True,True)"; |
|
17 by (mc_mucke_tac thy reach_rws 1); |
|
18 qed "reach_ex_thm1"; |
|
19 |
|
20 *) |
|
21 |