theory Test imports Pure begin type_notation (latex) "fun" (\(_/ \<^latex>\{\isasymlongrightarrow}\ignore{\aa\<^latex>\}\ _)\ [1, 0] 0) text \ @{typ [margin = 40, display] \'a \ 'a \ 'a \ 'a \ 'a \ 'a \ 'a \ 'a \ 'a \ 'a \ 'a \ 'a\} \ end