diff -r dd46544e259d -r 73b46b18c348 src/HOL/Library/README.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/README.html Wed Oct 18 23:31:16 2000 +0200 @@ -0,0 +1,114 @@ + + + + +
+ +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 output document: +\<Inter>, +\<Union>, +\<and>, +\<in>, +\<inter>, +\<not>, +\<noteq>, +\<notin>, +\<or>, +\<subset>, +\<subseteq>, +\<times>, +\<union>. + +