--- a/src/HOL/IMP/Transition.thy Wed Apr 14 13:28:46 2004 +0200
+++ b/src/HOL/IMP/Transition.thy Wed Apr 14 14:13:05 2004 +0200
@@ -35,6 +35,10 @@
"_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
"_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
+syntax (HTML output)
+ "_angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
+ "_angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
+
translations
"\<langle>c,s\<rangle>" == "(Some c, s)"
"\<langle>s\<rangle>" == "(None, s)"