theory Test
  imports Main
begin

section \<open>Formal comments in outer syntax\<close>

term x \<comment> \<open>informal text\<close>
term x \<comment> \<open>\<open>formal @{text}\<close>\<close>
term x \<comment> \<open>\<^verbatim>\<open>verbatim @{text}\<close>\<close>

term x \<^cancel>\<open>cancel\<close>


section \<open>Formal comments in inner syntax\<close>

term \<open>x \<comment> \<open>informal text\<close>\<close>
term \<open>x \<comment> \<open>\<open>formal @{text}\<close>\<close>\<close>
term \<open>x \<comment> \<open>\<^verbatim>\<open>verbatim @{text}\<close>\<close>\<close>

term \<open>x \<^cancel>\<open>cancel\<close>\<close>

end