]> matita.cs.unibo.it Git - helm.git/blob - helm/dtd/isonum.ent
Rel to hidden hypotheses are now printed as _hidden_n.
[helm.git] / helm / dtd / isonum.ent
1
2 <!--
3      File isonum.ent produced by the XSL script mmldtd.xsl
4      from input data in unicode.xml.
5
6      Please report any errors to 
7      David Carlisle <davidc@nag.co.uk>.
8
9      The numeric character values assigned to each entity
10      (should) match either official Unicode assignments
11      or assignments provisionally allocated by the
12      Unicode Consortium based on the characters in the `STIX'
13      propsal for mathematics. Note that these assignments
14      have not been ratified by the corresponding ISO
15      committee and thus should be considered liable to
16      change.
17
18      Entity names in this file are derived from files carrying the
19      following notice:
20
21      (C) International Organization for Standardization 1986
22      Permission to copy in any form is granted for use with
23      conforming SGML systems and applications as defined in
24      ISO 8879, provided this notice is included in all copies.
25
26 -->
27 <!--HELM: deleted the central &: 
28 <!ENTITY amp              "&#x26;&#x00026;" >-->
29 <!ENTITY amp              "&#x26;#x00026;" ><!--=ampersand -->
30 <!ENTITY apos             "&#x00027;" ><!--=apostrophe -->
31 <!ENTITY ast              "&#x0002A;" ><!--/ast B: =asterisk -->
32 <!ENTITY brvbar           "&#x000A6;" ><!--=broken (vertical) bar -->
33 <!ENTITY bsol             "&#x0005C;" ><!--/backslash =reverse solidus -->
34 <!ENTITY cent             "&#x000A2;" ><!--=cent sign -->
35 <!ENTITY colon            "&#x0003A;" ><!--/colon P: -->
36 <!ENTITY comma            "&#x0002C;" ><!--P: =comma -->
37 <!ENTITY commat           "&#x00040;" ><!--=commercial at -->
38 <!ENTITY copy             "&#x000A9;" ><!--=copyright sign -->
39 <!ENTITY curren           "&#x000A4;" ><!--=general currency sign -->
40 <!ENTITY darr             "&#x02193;" ><!--/downarrow A: =downward arrow -->
41 <!ENTITY deg              "&#x000B0;" ><!--=degree sign -->
42 <!ENTITY divide           "&#x000F7;" ><!--/div B: =divide sign -->
43 <!ENTITY dollar           "&#x00024;" ><!--=dollar sign -->
44 <!ENTITY equals           "&#x0003D;" ><!--=equals sign R: -->
45 <!ENTITY excl             "&#x00021;" ><!--=exclamation mark -->
46 <!ENTITY frac12           "&#x000BD;" ><!--=fraction one-half -->
47 <!ENTITY frac14           "&#x000BC;" ><!--=fraction one-quarter -->
48 <!ENTITY frac18           "&#x0215B;" ><!--=fraction one-eighth -->
49 <!ENTITY frac34           "&#x000BE;" ><!--=fraction three-quarters -->
50 <!ENTITY frac38           "&#x0215C;" ><!--=fraction three-eighths -->
51 <!ENTITY frac58           "&#x0215D;" ><!--=fraction five-eighths -->
52 <!ENTITY frac78           "&#x0215E;" ><!--=fraction seven-eighths -->
53 <!ENTITY gt               "&#x0003E;" ><!--=greater-than sign R: -->
54 <!ENTITY half             "&#x000BD;" ><!--=fraction one-half -->
55 <!ENTITY horbar           "&#x02015;" ><!--=horizontal bar -->
56 <!ENTITY hyphen           "&#x02010;" ><!--=hyphen -->
57 <!ENTITY iexcl            "&#x000A1;" ><!--=inverted exclamation mark -->
58 <!ENTITY iquest           "&#x000BF;" ><!--=inverted question mark -->
59 <!ENTITY laquo            "&#x000AB;" ><!--=angle quotation mark, left -->
60 <!ENTITY larr             "&#x02190;" ><!--/leftarrow /gets A: =leftward arrow -->
61 <!ENTITY lcub             "&#x0007B;" ><!--/lbrace O: =left curly bracket -->
62 <!ENTITY ldquo            "&#x0201C;" ><!--=double quotation mark, left -->
63 <!ENTITY lowbar           "&#x0005F;" ><!--=low line -->
64 <!ENTITY lpar             "&#x00028;" ><!--O: =left parenthesis -->
65 <!ENTITY lsqb             "&#x0005B;" ><!--/lbrack O: =left square bracket -->
66 <!ENTITY lsquo            "&#x02018;" ><!--=single quotation mark, left -->
67 <!--HELM: deleted the central &: 
68 <!ENTITY lt               "&#x26;&#x0003C;" >-->
69 <!ENTITY lt               "&#x26;#x0003C;" ><!--=less-than sign R: -->
70 <!ENTITY micro            "&#x000B5;" ><!--=micro sign -->
71 <!ENTITY middot           "&#x000B7;" ><!--/centerdot B: =middle dot -->
72 <!ENTITY nbsp             "&#x000A0;" ><!--=no break (required) space -->
73 <!ENTITY not              "&#x000AC;" ><!--/neg /lnot =not sign -->
74 <!ENTITY num              "&#x00023;" ><!--=number sign -->
75 <!ENTITY ohm              "&#x02126;" ><!--=ohm sign -->
76 <!ENTITY ordf             "&#x000AA;" ><!--=ordinal indicator, feminine -->
77 <!ENTITY ordm             "&#x000BA;" ><!--=ordinal indicator, masculine -->
78 <!ENTITY para             "&#x000B6;" ><!--=pilcrow (paragraph sign) -->
79 <!ENTITY percnt           "&#x00025;" ><!--=percent sign -->
80 <!ENTITY period           "&#x0002E;" ><!--=full stop, period -->
81 <!ENTITY plus             "&#x0002B;" ><!--=plus sign B: -->
82 <!ENTITY plusmn           "&#x000B1;" ><!--/pm B: =plus-or-minus sign -->
83 <!ENTITY pound            "&#x000A3;" ><!--=pound sign -->
84 <!ENTITY quest            "&#x0003F;" ><!--=question mark -->
85 <!ENTITY quot             "&#x00022;" ><!--=quotation mark -->
86 <!ENTITY raquo            "&#x000BB;" ><!--=angle quotation mark, right -->
87 <!ENTITY rarr             "&#x02192;" ><!--/rightarrow /to A: =rightward arrow -->
88 <!ENTITY rcub             "&#x0007D;" ><!--/rbrace C: =right curly bracket -->
89 <!ENTITY rdquo            "&#x0201D;" ><!--=double quotation mark, right -->
90 <!ENTITY reg              "&#x000AE;" ><!--/circledR =registered sign -->
91 <!ENTITY rpar             "&#x00029;" ><!--C: =right parenthesis -->
92 <!ENTITY rsqb             "&#x0005D;" ><!--/rbrack C: =right square bracket -->
93 <!ENTITY rsquo            "&#x02019;" ><!--=single quotation mark, right -->
94 <!ENTITY sect             "&#x000A7;" ><!--=section sign -->
95 <!ENTITY semi             "&#x0003B;" ><!--=semicolon P: -->
96 <!ENTITY shy              "&#x000AD;" ><!--=soft hyphen -->
97 <!ENTITY sol              "&#x0002F;" ><!--=solidus -->
98 <!ENTITY sung             "&#x0266A;" ><!--=music note (sung text sign) -->
99 <!ENTITY sup1             "&#x000B9;" ><!--=superscript one -->
100 <!ENTITY sup2             "&#x000B2;" ><!--=superscript two -->
101 <!ENTITY sup3             "&#x000B3;" ><!--=superscript three -->
102 <!ENTITY times            "&#x000D7;" ><!--/times B: =multiply sign -->
103 <!ENTITY trade            "&#x02122;" ><!--=trade mark sign -->
104 <!ENTITY uarr             "&#x02191;" ><!--/uparrow A: =upward arrow -->
105 <!ENTITY verbar           "&#x0007C;" ><!--/vert =vertical bar -->
106 <!ENTITY yen              "&#x000A5;" ><!--/yen =yen sign -->