19 |
19 |
20 syntax |
20 syntax |
21 "_Lstar" :: "two_seqe" ("(_)|L>(_)" [6,6] 5) |
21 "_Lstar" :: "two_seqe" ("(_)|L>(_)" [6,6] 5) |
22 "_Rstar" :: "two_seqe" ("(_)|R>(_)" [6,6] 5) |
22 "_Rstar" :: "two_seqe" ("(_)|R>(_)" [6,6] 5) |
23 |
23 |
24 ML {* |
24 ML \<open> |
25 fun star_tr c [s1, s2] = Const(c, dummyT) $ seq_tr s1 $ seq_tr s2; |
25 fun star_tr c [s1, s2] = Const(c, dummyT) $ seq_tr s1 $ seq_tr s2; |
26 fun star_tr' c [s1, s2] = Const(c, dummyT) $ seq_tr' s1 $ seq_tr' s2; |
26 fun star_tr' c [s1, s2] = Const(c, dummyT) $ seq_tr' s1 $ seq_tr' s2; |
27 *} |
27 \<close> |
28 |
28 |
29 parse_translation {* |
29 parse_translation \<open> |
30 [(@{syntax_const "_Lstar"}, K (star_tr @{const_syntax Lstar})), |
30 [(@{syntax_const "_Lstar"}, K (star_tr @{const_syntax Lstar})), |
31 (@{syntax_const "_Rstar"}, K (star_tr @{const_syntax Rstar}))] |
31 (@{syntax_const "_Rstar"}, K (star_tr @{const_syntax Rstar}))] |
32 *} |
32 \<close> |
33 |
33 |
34 print_translation {* |
34 print_translation \<open> |
35 [(@{const_syntax Lstar}, K (star_tr' @{syntax_const "_Lstar"})), |
35 [(@{const_syntax Lstar}, K (star_tr' @{syntax_const "_Lstar"})), |
36 (@{const_syntax Rstar}, K (star_tr' @{syntax_const "_Rstar"}))] |
36 (@{const_syntax Rstar}, K (star_tr' @{syntax_const "_Rstar"}))] |
37 *} |
37 \<close> |
38 |
38 |
39 defs |
39 defs |
40 strimp_def: "P --< Q == [](P --> Q)" |
40 strimp_def: "P --< Q == [](P --> Q)" |
41 streqv_def: "P >-< Q == (P --< Q) & (Q --< P)" |
41 streqv_def: "P >-< Q == (P --< Q) & (Q --< P)" |
42 |
42 |