equal
deleted
inserted
replaced
30 syntax |
30 syntax |
31 "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("<_,_>") |
31 "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("<_,_>") |
32 "_angle2" :: "state \<Rightarrow> com option \<times> state" ("<_>") |
32 "_angle2" :: "state \<Rightarrow> com option \<times> state" ("<_>") |
33 |
33 |
34 syntax (xsymbols) |
34 syntax (xsymbols) |
|
35 "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>") |
|
36 "_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>") |
|
37 |
|
38 syntax (HTML output) |
35 "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>") |
39 "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>") |
36 "_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>") |
40 "_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>") |
37 |
41 |
38 translations |
42 translations |
39 "\<langle>c,s\<rangle>" == "(Some c, s)" |
43 "\<langle>c,s\<rangle>" == "(Some c, s)" |