Addition of new theories should be done with some care, as the ``module system'' of Isabelle is rather simplistic. The following guidelines may be helpful to achieve maximum re-usability and minimum clashes with existing developments.
Note that syntax is global; qualified names loose syntax on output. Do not use ``exotic'' symbols for syntax (such as \<oplus>), but leave these for user applications.
The following ASCII symbols of HOL should be generally avoided: @, !, ?, ?!, %, better use SOME, ALL (or \<forall>), EX (or \<exists>), EX! (or \<exists>!), \<lambda>, respectively. Note that bracket notation [| |] looks bad in LaTeX output.
Some additional mathematical symbols are quite suitable for both readable sources and the output document: \<Inter>, \<Union>, \<and>, \<in>, \<inter>, \<le>, \<not>, \<noteq>, \<notin>, \<or>, \<subset>, \<subseteq>, \<times>, \<union>.