equal
deleted
inserted
replaced
11 by (simp_tac (MC_ss addsimps reach_rws) 1); |
11 by (simp_tac (MC_ss addsimps reach_rws) 1); |
12 |
12 |
13 (*show the current proof state using the model checker syntax*) |
13 (*show the current proof state using the model checker syntax*) |
14 setmp print_mode ["Eindhoven"] pr (); |
14 setmp print_mode ["Eindhoven"] pr (); |
15 |
15 |
16 (*actually invoke the model checker*) |
16 (* actually invoke the model checker *) |
17 by (mc_tac 1); |
17 (* try out after installing the model checker: see the README file *) |
|
18 |
|
19 (* by (mc_tac 1); *) |
18 |
20 |
19 (*qed "reach_ex_thm1";*) |
21 (*qed "reach_ex_thm1";*) |
20 |
22 |
21 |
23 |
22 |
24 |