equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 val reach_rws = [reach_def,INIT_def,N_def]; |
7 val reach_rws = [reach_def,INIT_def,N_def]; |
8 |
8 |
9 |
9 |
10 goal thy "reach (True,True,True)"; |
10 Goal "reach (True,True,True)"; |
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 |
21 (*qed "reach_ex_thm";*) |
21 (*qed "reach_ex_thm";*) |
22 |
22 |
23 |
23 |
24 |
24 |
25 (* just to make a proof in this file :-) *) |
25 (* just to make a proof in this file :-) *) |
26 goalw thy [INIT_def] "INIT (a,b,c) = (~a & ~b &~c)"; |
26 Goalw [INIT_def] "INIT (a,b,c) = (~a & ~b &~c)"; |
27 by (Simp_tac 1); |
27 by (Simp_tac 1); |
28 qed"init_state"; |
28 qed"init_state"; |