| changeset 4565 | ea467ce15040 |
| parent 4559 | 8e604d885b54 |
| child 5068 | fb28eaa07e01 |
| 4564:dc45cf21dbd2 | 4565:ea467ce15040 |
|---|---|
62 by (abstraction_tac 1); |
62 by (abstraction_tac 1); |
63 by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1); |
63 by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1); |
64 qed"TrivEx2_abstraction"; |
64 qed"TrivEx2_abstraction"; |
65 |
65 |
66 |
66 |
67 (* |
|
68 goal thy "validIOA aut_ioa (Box (Init (%(s,a,t). a= Some(Alarm(APonR)))) |
|
69 IMPLIES (Next (Init (%(s,a,t). info_comp(s) = APonR))))"; |
|
70 |
|
71 *) |
|
72 |