| changeset 13867 | 1fdecd15437f |
| parent 13857 | 11d7c5a8dbb7 |
| child 13875 | 12997e3ddd8d |
| 13866:b42d7983a822 | 13867:1fdecd15437f |
|---|---|
62 |
62 |
63 print_translation {* [("singl", singl_tr'),("star", star_tr')] *} |
63 print_translation {* [("singl", singl_tr'),("star", star_tr')] *} |
64 |
64 |
65 lemma "VARS H x y z w |
65 lemma "VARS H x y z w |
66 {[x\<mapsto>y] ** [z\<mapsto>w]} |
66 {[x\<mapsto>y] ** [z\<mapsto>w]} |
67 SKIP |
67 y := w |
68 {x \<noteq> z}" |
68 {x \<noteq> z}" |
69 apply vcg |
69 apply vcg |
70 apply(auto simp:star_def R_def singl_def) |
70 apply(auto simp:star_def R_def singl_def) |
71 done |
71 done |
72 |
72 |