]> matita.cs.unibo.it Git - helm.git/blob - helm/xml/dtd/isolat1.ent
- Procedural: we now reconstruct "let H := v in t" with "intros (1) H" when the goal...
[helm.git] / helm / xml / dtd / isolat1.ent
1
2 <!--
3      File isolat1.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
28 <!ENTITY aacute           "&#x000E1;" ><!--=small a, acute accent -->
29 <!ENTITY Aacute           "&#x000C1;" ><!--=capital A, acute accent -->
30 <!ENTITY acirc            "&#x000E2;" ><!--=small a, circumflex accent -->
31 <!ENTITY Acirc            "&#x000C2;" ><!--=capital A, circumflex accent -->
32 <!ENTITY aelig            "&#x000E6;" ><!--=small ae diphthong (ligature) -->
33 <!ENTITY AElig            "&#x000C6;" ><!--=capital AE diphthong (ligature) -->
34 <!ENTITY agrave           "&#x000E0;" ><!--=small a, grave accent -->
35 <!ENTITY Agrave           "&#x000C0;" ><!--=capital A, grave accent -->
36 <!ENTITY aring            "&#x000E5;" ><!--=small a, ring -->
37 <!ENTITY Aring            "&#x000C5;" ><!--=capital A, ring -->
38 <!ENTITY atilde           "&#x000E3;" ><!--=small a, tilde -->
39 <!ENTITY Atilde           "&#x000C3;" ><!--=capital A, tilde -->
40 <!ENTITY auml             "&#x000E4;" ><!--=small a, dieresis or umlaut mark -->
41 <!ENTITY Auml             "&#x000C4;" ><!--=capital A, dieresis or umlaut mark -->
42 <!ENTITY ccedil           "&#x000E7;" ><!--=small c, cedilla -->
43 <!ENTITY Ccedil           "&#x000C7;" ><!--=capital C, cedilla -->
44 <!ENTITY eacute           "&#x000E9;" ><!--=small e, acute accent -->
45 <!ENTITY Eacute           "&#x000C9;" ><!--=capital E, acute accent -->
46 <!ENTITY ecirc            "&#x000EA;" ><!--=small e, circumflex accent -->
47 <!ENTITY Ecirc            "&#x000CA;" ><!--=capital E, circumflex accent -->
48 <!ENTITY egrave           "&#x000E8;" ><!--=small e, grave accent -->
49 <!ENTITY Egrave           "&#x000C8;" ><!--=capital E, grave accent -->
50 <!ENTITY eth              "&#x000F0;" ><!--=small eth, Icelandic -->
51 <!ENTITY ETH              "&#x000D0;" ><!--=capital Eth, Icelandic -->
52 <!ENTITY euml             "&#x000EB;" ><!--=small e, dieresis or umlaut mark -->
53 <!ENTITY Euml             "&#x000CB;" ><!--=capital E, dieresis or umlaut mark -->
54 <!ENTITY iacute           "&#x000ED;" ><!--=small i, acute accent -->
55 <!ENTITY Iacute           "&#x000CD;" ><!--=capital I, acute accent -->
56 <!ENTITY icirc            "&#x000EE;" ><!--=small i, circumflex accent -->
57 <!ENTITY Icirc            "&#x000CE;" ><!--=capital I, circumflex accent -->
58 <!ENTITY igrave           "&#x000EC;" ><!--=small i, grave accent -->
59 <!ENTITY Igrave           "&#x000CC;" ><!--=capital I, grave accent -->
60 <!ENTITY iuml             "&#x000EF;" ><!--=small i, dieresis or umlaut mark -->
61 <!ENTITY Iuml             "&#x000CF;" ><!--=capital I, dieresis or umlaut mark -->
62 <!ENTITY ntilde           "&#x000F1;" ><!--=small n, tilde -->
63 <!ENTITY Ntilde           "&#x000D1;" ><!--=capital N, tilde -->
64 <!ENTITY oacute           "&#x000F3;" ><!--=small o, acute accent -->
65 <!ENTITY Oacute           "&#x000D3;" ><!--=capital O, acute accent -->
66 <!ENTITY ocirc            "&#x000F4;" ><!--=small o, circumflex accent -->
67 <!ENTITY Ocirc            "&#x000D4;" ><!--=capital O, circumflex accent -->
68 <!ENTITY ograve           "&#x000F2;" ><!--=small o, grave accent -->
69 <!ENTITY Ograve           "&#x000D2;" ><!--=capital O, grave accent -->
70 <!ENTITY oslash           "&#x000F8;" ><!--latin small letter o with stroke -->
71 <!ENTITY Oslash           "&#x000D8;" ><!--=capital O, slash -->
72 <!ENTITY otilde           "&#x000F5;" ><!--=small o, tilde -->
73 <!ENTITY Otilde           "&#x000D5;" ><!--=capital O, tilde -->
74 <!ENTITY ouml             "&#x000F6;" ><!--=small o, dieresis or umlaut mark -->
75 <!ENTITY Ouml             "&#x000D6;" ><!--=capital O, dieresis or umlaut mark -->
76 <!ENTITY szlig            "&#x000DF;" ><!--=small sharp s, German (sz ligature) -->
77 <!ENTITY thorn            "&#x000FE;" ><!--=small thorn, Icelandic -->
78 <!ENTITY THORN            "&#x000DE;" ><!--=capital THORN, Icelandic -->
79 <!ENTITY uacute           "&#x000FA;" ><!--=small u, acute accent -->
80 <!ENTITY Uacute           "&#x000DA;" ><!--=capital U, acute accent -->
81 <!ENTITY ucirc            "&#x000FB;" ><!--=small u, circumflex accent -->
82 <!ENTITY Ucirc            "&#x000DB;" ><!--=capital U, circumflex accent -->
83 <!ENTITY ugrave           "&#x000F9;" ><!--=small u, grave accent -->
84 <!ENTITY Ugrave           "&#x000D9;" ><!--=capital U, grave accent -->
85 <!ENTITY uuml             "&#x000FC;" ><!--=small u, dieresis or umlaut mark -->
86 <!ENTITY Uuml             "&#x000DC;" ><!--=capital U, dieresis or umlaut mark -->
87 <!ENTITY yacute           "&#x000FD;" ><!--=small y, acute accent -->
88 <!ENTITY Yacute           "&#x000DD;" ><!--=capital Y, acute accent -->
89 <!ENTITY yuml             "&#x000FF;" ><!--=small y, dieresis or umlaut mark -->