- -Note that syntax is global; qualified names lose 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>. -