Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Admin/xsymbol/xsymb1_14.bdf
changeset 10048 eb9983e554fd 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/xsymbol/xsymb1_14.bdf	Thu Sep 21 12:26:37 2000 +0200
@@ -0,0 +1,2796 @@
+STARTFONT 2.1
+COMMENT xsymb1_14.bdf --- additional font for package x-symbol
+COMMENT
+COMMENT Copyright (C) 1996-1999 Free Software Foundation, Inc.
+COMMENT
+COMMENT Author: Christoph Wedler <wedler@fmi.uni-passau.de>
+COMMENT Version: $Id$
+COMMENT Keywords: fonts, WYSIWYG, LaTeX, HTML, wp, math
+COMMENT X-URL: http://www.fmi.uni-passau.de/~wedler/x-symbol/
+COMMENT
+COMMENT This font is free software; you can redistribute it and/or modify
+COMMENT it under the terms of the GNU General Public License as published by
+COMMENT the Free Software Foundation; either version 2, or (at your option)
+COMMENT any later version.
+COMMENT
+COMMENT This program is distributed in the hope that it will be useful,
+COMMENT but WITHOUT ANY WARRANTY; without even the implied warranty of
+COMMENT MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+COMMENT GNU General Public License for more details.
+COMMENT
+COMMENT You should have received a copy of the GNU General Public License
+COMMENT along with this program; if not, write to the Free Software
+COMMENT Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
+COMMENT 
+COMMENT 
+FONT -XSYMB-XSymb1-Medium-R-Normal--14-140-75-75-P-85-XSYMB-XSymb1
+SIZE 14 75 75
+FONTBOUNDINGBOX 19 16 2 -3
+STARTPROPERTIES 23
+FONTNAME_REGISTRY ""
+FAMILY_NAME "XSymb1"
+FOUNDRY "XSYMB"
+WEIGHT_NAME "Medium"
+SETWIDTH_NAME "Normal"
+SLANT "R"
+ADD_STYLE_NAME ""
+PIXEL_SIZE 14
+POINT_SIZE 140
+RESOLUTION_X 75
+RESOLUTION_Y 75
+SPACING "P"
+AVERAGE_WIDTH 85
+CHARSET_REGISTRY "XSYMB"
+CHARSET_ENCODING "XSymb1"
+CHARSET_COLLECTIONS "XSymb1"
+FONT_DESCENT 3
+FONT_ASCENT 13
+CAP_HEIGHT 10
+X_HEIGHT 7
+FACE_NAME "XSymb1"
+DEVICE_FONT_NAME "XSymb1"
+COPYRIGHT "1997-1999 Free Software Foundation, Inc."
+ENDPROPERTIES
+CHARS 169
+STARTCHAR verticaldots
+ENCODING 33
+SWIDTH 250 0
+DWIDTH 5 0
+BBX 1 10 2 0
+BITMAP
+80
+80
+00
+00
+80
+80
+00
+00
+80
+80
+ENDCHAR
+STARTCHAR backslash1
+ENCODING 34
+SWIDTH 250 0
+DWIDTH 7 0
+BBX 6 13 0 -2
+BITMAP
+80
+c0
+40
+60
+20
+30
+10
+18
+08
+0c
+04
+00
+7c
+ENDCHAR
+STARTCHAR dagger
+ENCODING 35
+SWIDTH 250 0
+DWIDTH 7 0
+BBX 5 13 1 -2
+BITMAP
+70
+70
+20
+f8
+20
+70
+70
+70
+70
+70
+20
+20
+20
+ENDCHAR
+STARTCHAR percent2
+ENCODING 38
+SWIDTH 833 0
+DWIDTH 12 0
+BBX 9 10 1 0
+BITMAP
+7980
+9700
+9200
+9400
+6c00
+1b00
+1480
+2480
+4480
+c300
+ENDCHAR
+STARTCHAR guilsinglright
+ENCODING 39
+SWIDTH 250 0
+DWIDTH 5 0
+BBX 3 5 1 2
+BITMAP
+80
+40
+20
+40
+80
+ENDCHAR
+STARTCHAR NG
+ENCODING 40
+SWIDTH 250 0
+DWIDTH 10 0
+BBX 8 11 1 0
+BITMAP
+bc
+c2
+83
+81
+81
+81
+81
+81
+81
+91
+9e
+ENDCHAR
+STARTCHAR OE
+ENCODING 41
+SWIDTH 1000 0
+DWIDTH 15 0
+BBX 13 11 1 0
+BITMAP
+1ff8
+6300
+4100
+8100
+8100
+81f8
+8100
+8100
+4100
+6300
+1ff8
+ENDCHAR
+STARTCHAR dotlessj
+ENCODING 42
+SWIDTH 250 0
+DWIDTH 5 0
+BBX 4 11 0 -3
+BITMAP
+10
+10
+10
+10
+10
+10
+10
+10
+10
+10
+e0
+ENDCHAR
+STARTCHAR ng
+ENCODING 43
+SWIDTH 250 0
+DWIDTH 8 0
+BBX 6 11 1 -3
+BITMAP
+b8
+cc
+84
+84
+84
+84
+84
+84
+04
+14
+18
+ENDCHAR
+STARTCHAR oe
+ENCODING 44
+SWIDTH 944 0
+DWIDTH 13 0
+BBX 11 8 1 0
+BITMAP
+7bc0
+ce60
+8420
+87e0
+8400
+8400
+ce60
+7bc0
+ENDCHAR
+STARTCHAR sharp
+ENCODING 45
+SWIDTH 250 0
+DWIDTH 8 0
+BBX 6 12 1 -1
+BITMAP
+08
+4c
+5c
+78
+e8
+c8
+4c
+5c
+78
+e8
+c0
+40
+ENDCHAR
+STARTCHAR ceilingleft
+ENCODING 46
+SWIDTH 480 0
+DWIDTH 7 0
+BBX 5 13 1 -2
+BITMAP
+f8
+f8
+80
+80
+80
+80
+80
+80
+80
+80
+80
+80
+80
+ENDCHAR
+STARTCHAR ceilingright
+ENCODING 47
+SWIDTH 480 0
+DWIDTH 7 0
+BBX 5 13 1 -2
+BITMAP
+f8
+f8
+08
+08
+08
+08
+08
+08
+08
+08
+08
+08
+08
+ENDCHAR
+STARTCHAR zero
+ENCODING 48
+SWIDTH 500 0
+DWIDTH 7 0
+BBX 6 10 0 0
+BITMAP
+78
+cc
+84
+84
+84
+84
+84
+84
+cc
+78
+ENDCHAR
+STARTCHAR one
+ENCODING 49
+SWIDTH 500 0
+DWIDTH 7 0
+BBX 5 10 1 0
+BITMAP
+20
+e0
+20
+20
+20
+20
+20
+20
+20
+f8
+ENDCHAR
+STARTCHAR two
+ENCODING 50
+SWIDTH 500 0
+DWIDTH 7 0
+BBX 6 10 0 0
+BITMAP
+70
+d8
+88
+08
+18
+10
+20
+40
+c4
+fc
+ENDCHAR
+STARTCHAR three
+ENCODING 51
+SWIDTH 500 0
+DWIDTH 7 0
+BBX 6 10 0 0
+BITMAP
+78
+cc
+84
+0c
+38
+0c
+04
+04
+cc
+78
+ENDCHAR
+STARTCHAR four
+ENCODING 52
+SWIDTH 500 0
+DWIDTH 7 0
+BBX 6 10 0 0
+BITMAP
+08
+18
+18
+28
+68
+48
+88
+fc
+08
+08
+ENDCHAR
+STARTCHAR five
+ENCODING 53
+SWIDTH 500 0
+DWIDTH 7 0
+BBX 5 10 1 0
+BITMAP
+78
+40
+80
+e0
+30
+18
+08
+08
+90
+e0
+ENDCHAR
+STARTCHAR six
+ENCODING 54
+SWIDTH 500 0
+DWIDTH 7 0
+BBX 6 10 0 0
+BITMAP
+1c
+30
+40
+40
+f8
+8c
+84
+84
+cc
+78
+ENDCHAR
+STARTCHAR seven
+ENCODING 55
+SWIDTH 500 0
+DWIDTH 7 0
+BBX 6 10 1 0
+BITMAP
+fc
+84
+08
+08
+10
+10
+20
+20
+40
+40
+ENDCHAR
+STARTCHAR eight
+ENCODING 56
+SWIDTH 500 0
+DWIDTH 7 0
+BBX 5 10 1 0
+BITMAP
+70
+d8
+88
+88
+70
+88
+88
+88
+d8
+70
+ENDCHAR
+STARTCHAR nine
+ENCODING 57
+SWIDTH 500 0
+DWIDTH 7 0
+BBX 6 10 0 0
+BITMAP
+78
+cc
+84
+84
+c4
+78
+18
+10
+60
+c0
+ENDCHAR
+STARTCHAR star
+ENCODING 58
+SWIDTH 250 0
+DWIDTH 7 0
+BBX 5 10 1 2
+BITMAP
+00
+00
+00
+00
+20
+a8
+f8
+70
+50
+d8
+ENDCHAR
+STARTCHAR lozenge1
+ENCODING 59
+SWIDTH 250 0
+DWIDTH 11 0
+BBX 11 11 0 -1
+BITMAP
+0400
+0e00
+1b00
+3180
+60c0
+c060
+60c0
+3180
+1b00
+0e00
+0400
+ENDCHAR
+STARTCHAR braceleft2
+ENCODING 60
+SWIDTH 480 0
+DWIDTH 8 0
+BBX 6 13 1 -2
+BITMAP
+1c
+30
+30
+30
+30
+64
+cc
+64
+30
+30
+30
+30
+1c
+ENDCHAR
+STARTCHAR circleslash
+ENCODING 61
+SWIDTH 768 0
+DWIDTH 11 0
+BBX 9 9 1 0
+BITMAP
+1c00
+6300
+4300
+8480
+8880
+9080
+6100
+6300
+1c00
+ENDCHAR
+STARTCHAR braceright2
+ENCODING 62
+SWIDTH 480 0
+DWIDTH 8 0
+BBX 6 13 1 -2
+BITMAP
+e0
+30
+30
+30
+30
+98
+cc
+98
+30
+30
+30
+30
+e0
+ENDCHAR
+STARTCHAR triangle1
+ENCODING 63
+SWIDTH 713 0
+DWIDTH 9 0
+BBX 7 7 1 1
+BITMAP
+10
+38
+28
+44
+44
+82
+fe
+ENDCHAR
+STARTCHAR smltriangleright
+ENCODING 64
+SWIDTH 713 0
+DWIDTH 9 0
+BBX 7 7 1 1
+BITMAP
+c0
+b0
+8c
+86
+8c
+b0
+c0
+ENDCHAR
+STARTCHAR triangleleft
+ENCODING 65
+SWIDTH 713 0
+DWIDTH 11 0
+BBX 9 9 1 0
+BITMAP
+0180
+0680
+1c80
+7080
+c080
+7080
+1c80
+0680
+0180
+ENDCHAR
+STARTCHAR triangle
+ENCODING 66
+SWIDTH 713 0
+DWIDTH 11 0
+BBX 9 11 1 0
+BITMAP
+0800
+0800
+1c00
+1400
+3600
+2200
+6300
+4100
+c180
+8080
+ff80
+ENDCHAR
+STARTCHAR triangleright
+ENCODING 67
+SWIDTH 713 0
+DWIDTH 11 0
+BBX 9 9 1 0
+BITMAP
+c000
+b000
+9c00
+8700
+8180
+8700
+9c00
+b000
+c000
+ENDCHAR
+STARTCHAR trianglelefteq
+ENCODING 68
+SWIDTH 713 0
+DWIDTH 11 0
+BBX 9 11 1 -1
+BITMAP
+0180
+0680
+1c80
+7080
+c080
+7080
+1c80
+0680
+0180
+0000
+7f80
+ENDCHAR
+STARTCHAR trianglerighteq
+ENCODING 69
+SWIDTH 713 0
+DWIDTH 11 0
+BBX 9 11 1 -1
+BITMAP
+c000
+b000
+9c00
+8700
+8180
+8700
+9c00
+b000
+c000
+0000
+ff00
+ENDCHAR
+STARTCHAR periodcentered2
+ENCODING 70
+SWIDTH 250 0
+DWIDTH 7 0
+BBX 5 8 1 -2
+BITMAP
+40
+40
+00
+00
+00
+00
+00
+f8
+ENDCHAR
+STARTCHAR dotequal
+ENCODING 71
+SWIDTH 549 0
+DWIDTH 9 0
+BBX 7 6 1 2
+BITMAP
+10
+10
+00
+fe
+00
+fe
+ENDCHAR
+STARTCHAR wrong
+ENCODING 72
+SWIDTH 250 0
+DWIDTH 5 0
+BBX 3 11 1 -1
+BITMAP
+00
+c0
+20
+20
+20
+40
+40
+80
+80
+80
+60
+ENDCHAR
+STARTCHAR natural
+ENCODING 73
+SWIDTH 250 0
+DWIDTH 7 0
+BBX 5 13 1 -2
+BITMAP
+80
+80
+98
+b8
+e8
+c8
+88
+98
+b8
+e8
+c8
+08
+08
+ENDCHAR
+STARTCHAR flat
+ENCODING 74
+SWIDTH 250 0
+DWIDTH 7 0
+BBX 5 11 1 0
+BITMAP
+80
+80
+80
+f0
+98
+98
+98
+b0
+b0
+e0
+c0
+ENDCHAR
+STARTCHAR epsilon1
+ENCODING 75
+SWIDTH 439 0
+DWIDTH 6 0
+BBX 5 7 1 0
+BITMAP
+70
+c8
+80
+60
+80
+c8
+70
+ENDCHAR
+STARTCHAR hbarmath
+ENCODING 76
+SWIDTH 250 0
+DWIDTH 8 0
+BBX 7 11 0 0
+BITMAP
+00
+40
+f8
+40
+5c
+66
+42
+42
+42
+42
+42
+ENDCHAR
+STARTCHAR imath
+ENCODING 77
+SWIDTH 329 0
+DWIDTH 5 0
+BBX 4 7 0 0
+BITMAP
+70
+b0
+30
+20
+60
+60
+70
+ENDCHAR
+STARTCHAR kappa1
+ENCODING 78
+SWIDTH 329 0
+DWIDTH 9 0
+BBX 7 7 1 0
+BITMAP
+e2
+a6
+2c
+38
+68
+ca
+8e
+ENDCHAR
+STARTCHAR jmath
+ENCODING 79
+SWIDTH 329 0
+DWIDTH 7 0
+BBX 6 10 0 -3
+BITMAP
+3c
+4c
+0c
+0c
+18
+18
+18
+98
+f0
+60
+ENDCHAR
+STARTCHAR ell
+ENCODING 80
+SWIDTH 250 0
+DWIDTH 6 0
+BBX 5 11 0 0
+BITMAP
+00
+30
+48
+48
+48
+48
+48
+50
+e0
+48
+30
+ENDCHAR
+STARTCHAR amalg
+ENCODING 81
+SWIDTH 768 0
+DWIDTH 11 0
+BBX 9 10 1 0
+BITMAP
+e380
+4100
+4100
+4100
+4100
+4100
+4100
+4100
+4100
+ff80
+ENDCHAR
+STARTCHAR rho1
+ENCODING 82
+SWIDTH 549 0
+DWIDTH 8 0
+BBX 6 10 1 -3
+BITMAP
+78
+cc
+84
+84
+84
+cc
+b8
+80
+80
+78
+ENDCHAR
+STARTCHAR top
+ENCODING 83
+SWIDTH 658 0
+DWIDTH 10 0
+BBX 9 10 0 -1
+BITMAP
+ff80
+0800
+0800
+0800
+0800
+0800
+0800
+0800
+0800
+0800
+ENDCHAR
+STARTCHAR Mho
+ENCODING 84
+SWIDTH 768 0
+DWIDTH 11 0
+BBX 10 10 0 0
+BITMAP
+f3c0
+9240
+2100
+4080
+4080
+4080
+4080
+2100
+3300
+0c00
+ENDCHAR
+STARTCHAR floorleft
+ENCODING 85
+SWIDTH 480 0
+DWIDTH 7 0
+BBX 5 13 1 -2
+BITMAP
+80
+80
+80
+80
+80
+80
+80
+80
+80
+80
+80
+f8
+f8
+ENDCHAR
+STARTCHAR floorright
+ENCODING 86
+SWIDTH 480 0
+DWIDTH 7 0
+BBX 5 13 1 -2
+BITMAP
+08
+08
+08
+08
+08
+08
+08
+08
+08
+08
+08
+f8
+f8
+ENDCHAR
+STARTCHAR perpendicular1
+ENCODING 87
+SWIDTH 658 0
+DWIDTH 9 0
+BBX 7 7 1 1
+BITMAP
+10
+10
+10
+10
+10
+10
+fe
+ENDCHAR
+STARTCHAR box
+ENCODING 88
+SWIDTH 250 0
+DWIDTH 10 0
+BBX 8 9 1 0
+BITMAP
+ff
+81
+81
+81
+81
+81
+81
+81
+ff
+ENDCHAR
+STARTCHAR asciicircum1
+ENCODING 89
+SWIDTH 200 0
+DWIDTH 9 0
+BBX 7 13 1 -2
+BITMAP
+10
+38
+6c
+c6
+82
+00
+00
+00
+00
+00
+00
+00
+7c
+ENDCHAR
+STARTCHAR asciitilde1
+ENCODING 90
+SWIDTH 200 0
+DWIDTH 9 0
+BBX 7 13 1 -2
+BITMAP
+60
+b2
+9a
+0c
+00
+00
+00
+00
+00
+00
+00
+00
+7c
+ENDCHAR
+STARTCHAR leadsto
+ENCODING 91
+SWIDTH 987 0
+DWIDTH 14 0
+BBX 12 7 1 1
+BITMAP
+0080
+0040
+4220
+e7f0
+1820
+0040
+0080
+ENDCHAR
+STARTCHAR quotedbl1
+ENCODING 92
+SWIDTH 355 0
+DWIDTH 5 0
+BBX 3 3 1 8
+BITMAP
+a0
+a0
+a0
+ENDCHAR
+STARTCHAR longarrowleft
+ENCODING 93
+SWIDTH 987 0
+DWIDTH 21 0
+BBX 19 7 1 1
+BITMAP
+100000
+200000
+400000
+ffffe0
+400000
+200000
+100000
+ENDCHAR
+STARTCHAR arrowupdown
+ENCODING 94
+SWIDTH 603 0
+DWIDTH 9 0
+BBX 7 12 1 -2
+BITMAP
+10
+38
+54
+92
+10
+10
+10
+10
+92
+54
+38
+10
+ENDCHAR
+STARTCHAR longarrowright
+ENCODING 95
+SWIDTH 987 0
+DWIDTH 21 0
+BBX 19 7 1 1
+BITMAP
+000100
+000080
+000040
+ffffe0
+000040
+000080
+000100
+ENDCHAR
+STARTCHAR longmapsto
+ENCODING 96
+SWIDTH 987 0
+DWIDTH 21 0
+BBX 19 7 1 1
+BITMAP
+000100
+800080
+800040
+ffffe0
+800040
+800080
+000100
+ENDCHAR
+STARTCHAR longarrowdblboth
+ENCODING 97
+SWIDTH 987 0
+DWIDTH 21 0
+BBX 19 7 1 1
+BITMAP
+100100
+200080
+7fffc0
+c00060
+7fffc0
+200080
+100100
+ENDCHAR
+STARTCHAR longarrowdblleft
+ENCODING 98
+SWIDTH 987 0
+DWIDTH 21 0
+BBX 19 7 1 1
+BITMAP
+100000
+200000
+7fffe0
+c00000
+7fffe0
+200000
+100000
+ENDCHAR
+STARTCHAR arrowdblupdown
+ENCODING 99
+SWIDTH 603 0
+DWIDTH 9 0
+BBX 7 12 1 -2
+BITMAP
+10
+38
+6c
+aa
+28
+28
+28
+28
+aa
+6c
+38
+10
+ENDCHAR
+STARTCHAR longarrowdblright
+ENCODING 100
+SWIDTH 987 0
+DWIDTH 21 0
+BBX 19 7 1 1
+BITMAP
+000100
+000080
+ffffc0
+000060
+ffffc0
+000080
+000100
+ENDCHAR
+STARTCHAR mapsto
+ENCODING 101
+SWIDTH 987 0
+DWIDTH 14 0
+BBX 12 7 1 1
+BITMAP
+0080
+8040
+8020
+fff0
+8020
+8040
+0080
+ENDCHAR
+STARTCHAR iff
+ENCODING 102
+SWIDTH 987 0
+DWIDTH 23 0
+BBX 19 9 2 1
+BITMAP
+02d800
+009000
+12d900
+229080
+7a93c0
+c00060
+7fffc0
+200080
+100100
+ENDCHAR
+STARTCHAR hookleftarrow
+ENCODING 103
+SWIDTH 494 0
+DWIDTH 14 0
+BBX 12 7 1 1
+BITMAP
+1020
+2010
+4010
+ffe0
+4000
+2000
+1000
+ENDCHAR
+STARTCHAR hookrightarrow
+ENCODING 104
+SWIDTH 494 0
+DWIDTH 14 0
+BBX 12 7 1 1
+BITMAP
+4080
+8040
+8020
+7ff0
+0020
+0040
+0080
+ENDCHAR
+STARTCHAR arrownortheast
+ENCODING 105
+SWIDTH 494 0
+DWIDTH 14 0
+BBX 12 12 1 -2
+BITMAP
+01f0
+0030
+0050
+0090
+0110
+0200
+0400
+0800
+1000
+2000
+4000
+8000
+ENDCHAR
+STARTCHAR arrowsoutheast
+ENCODING 106
+SWIDTH 494 0
+DWIDTH 14 0
+BBX 12 12 1 -2
+BITMAP
+8000
+4000
+2000
+1000
+0800
+0400
+0200
+0110
+0090
+0050
+0030
+01f0
+ENDCHAR
+STARTCHAR arrownorthwest
+ENCODING 107
+SWIDTH 494 0
+DWIDTH 14 0
+BBX 12 12 1 -2
+BITMAP
+f800
+c000
+a000
+9000
+8800
+0400
+0200
+0100
+0080
+0040
+0020
+0010
+ENDCHAR
+STARTCHAR arrowsouthwest
+ENCODING 108
+SWIDTH 494 0
+DWIDTH 14 0
+BBX 12 12 1 -2
+BITMAP
+0010
+0020
+0040
+0080
+0100
+0200
+0400
+8800
+9000
+a000
+c000
+f800
+ENDCHAR
+STARTCHAR rightleftharpoons
+ENCODING 109
+SWIDTH 494 0
+DWIDTH 14 0
+BBX 12 9 1 0
+BITMAP
+0080
+0040
+0020
+fff0
+0000
+fff0
+4000
+2000
+1000
+ENDCHAR
+STARTCHAR leftharpoondown
+ENCODING 110
+SWIDTH 494 0
+DWIDTH 14 0
+BBX 12 4 1 2
+BITMAP
+fff0
+4000
+2000
+1000
+ENDCHAR
+STARTCHAR rightharpoondown
+ENCODING 111
+SWIDTH 494 0
+DWIDTH 14 0
+BBX 12 4 1 2
+BITMAP
+fff0
+0020
+0040
+0080
+ENDCHAR
+STARTCHAR leftharpoonup
+ENCODING 112
+SWIDTH 494 0
+DWIDTH 14 0
+BBX 12 4 1 4
+BITMAP
+1000
+2000
+4000
+fff0
+ENDCHAR
+STARTCHAR rightharpoonup
+ENCODING 113
+SWIDTH 494 0
+DWIDTH 14 0
+BBX 12 4 1 4
+BITMAP
+0080
+0040
+0020
+fff0
+ENDCHAR
+STARTCHAR bardbl
+ENCODING 114
+SWIDTH 480 0
+DWIDTH 6 0
+BBX 4 13 1 -2
+BITMAP
+90
+90
+90
+90
+90
+90
+90
+90
+90
+90
+90
+90
+90
+ENDCHAR
+STARTCHAR bardbl1
+ENCODING 115
+SWIDTH 480 0
+DWIDTH 5 0
+BBX 3 8 1 1
+BITMAP
+a0
+a0
+a0
+a0
+a0
+a0
+a0
+a0
+ENDCHAR
+STARTCHAR backslash2
+ENCODING 116
+SWIDTH 250 0
+DWIDTH 9 0
+BBX 7 14 1 -2
+BITMAP
+80
+c0
+c0
+60
+60
+30
+30
+18
+18
+0c
+0c
+06
+06
+02
+ENDCHAR
+STARTCHAR backslash3
+ENCODING 117
+SWIDTH 250 0
+DWIDTH 7 0
+BBX 5 8 1 1
+BITMAP
+00
+80
+80
+40
+20
+10
+08
+08
+ENDCHAR
+STARTCHAR diagonaldots
+ENCODING 118
+SWIDTH 250 0
+DWIDTH 11 0
+BBX 9 10 1 0
+BITMAP
+8000
+8000
+0000
+0000
+0800
+0800
+0000
+0000
+0080
+0080
+ENDCHAR
+STARTCHAR simequal
+ENCODING 119
+SWIDTH 549 0
+DWIDTH 9 0
+BBX 7 7 1 0
+BITMAP
+62
+d2
+96
+8c
+00
+00
+fe
+ENDCHAR
+STARTCHAR digamma
+ENCODING 120
+SWIDTH 500 0
+DWIDTH 10 0
+BBX 8 11 1 -2
+BITMAP
+3f
+30
+30
+70
+60
+78
+60
+e0
+c0
+c0
+c0
+ENDCHAR
+STARTCHAR asym
+ENCODING 121
+SWIDTH 250 0
+DWIDTH 11 0
+BBX 9 7 1 1
+BITMAP
+8080
+4100
+3e00
+0000
+3e00
+4100
+8080
+ENDCHAR
+STARTCHAR minusplus
+ENCODING 122
+SWIDTH 250 0
+DWIDTH 7 0
+BBX 5 9 1 1
+BITMAP
+00
+00
+f8
+00
+20
+20
+f8
+20
+20
+ENDCHAR
+STARTCHAR less2
+ENCODING 123
+SWIDTH 549 0
+DWIDTH 8 0
+BBX 7 7 1 0
+BITMAP
+02
+0c
+30
+c0
+30
+0c
+02
+ENDCHAR
+STARTCHAR bowtie
+ENCODING 124
+SWIDTH 250 0
+DWIDTH 9 0
+BBX 7 7 1 1
+BITMAP
+82
+c6
+aa
+92
+aa
+c6
+82
+ENDCHAR
+STARTCHAR greater
+ENCODING 125
+SWIDTH 549 0
+DWIDTH 8 0
+BBX 7 7 0 0
+BITMAP
+80
+60
+18
+06
+18
+60
+80
+ENDCHAR
+STARTCHAR centraldots
+ENCODING 126
+SWIDTH 1000 0
+DWIDTH 13 0
+BBX 9 2 2 4
+BITMAP
+8880
+8880
+ENDCHAR
+STARTCHAR visiblespace
+ENCODING 160
+SWIDTH 250 0
+DWIDTH 8 0
+BBX 6 3 1 -1
+BITMAP
+00
+84
+fc
+ENDCHAR
+STARTCHAR dagger1
+ENCODING 161
+SWIDTH 250 0
+DWIDTH 7 0
+BBX 5 9 1 0
+BITMAP
+20
+20
+f8
+20
+20
+70
+70
+20
+20
+ENDCHAR
+STARTCHAR circledot
+ENCODING 162
+SWIDTH 768 0
+DWIDTH 11 0
+BBX 9 9 1 0
+BITMAP
+1c00
+6300
+4100
+8080
+8880
+8080
+4100
+6300
+1c00
+ENDCHAR
+STARTCHAR propersqsuperset
+ENCODING 163
+SWIDTH 713 0
+DWIDTH 10 0
+BBX 8 7 1 1
+BITMAP
+ff
+01
+01
+01
+01
+01
+ff
+ENDCHAR
+STARTCHAR reflexsqsuperset
+ENCODING 164
+SWIDTH 713 0
+DWIDTH 10 0
+BBX 8 9 1 0
+BITMAP
+ff
+01
+01
+01
+01
+01
+ff
+00
+ff
+ENDCHAR
+STARTCHAR gradient1
+ENCODING 165
+SWIDTH 713 0
+DWIDTH 9 0
+BBX 7 7 1 1
+BITMAP
+fe
+82
+44
+44
+28
+28
+10
+ENDCHAR
+STARTCHAR propersqsubset
+ENCODING 166
+SWIDTH 713 0
+DWIDTH 10 0
+BBX 8 7 1 1
+BITMAP
+ff
+80
+80
+80
+80
+80
+ff
+ENDCHAR
+STARTCHAR reflexsqsubset
+ENCODING 167
+SWIDTH 713 0
+DWIDTH 10 0
+BBX 8 9 1 0
+BITMAP
+ff
+80
+80
+80
+80
+80
+ff
+00
+ff
+ENDCHAR
+STARTCHAR smllozenge
+ENCODING 168
+SWIDTH 494 0
+DWIDTH 9 0
+BBX 7 7 1 1
+BITMAP
+10
+28
+44
+82
+44
+28
+10
+ENDCHAR
+STARTCHAR lessless
+ENCODING 169
+SWIDTH 549 0
+DWIDTH 12 0
+BBX 10 7 1 1
+BITMAP
+0440
+1980
+6600
+8800
+6600
+1980
+0440
+ENDCHAR
+STARTCHAR greatergreater
+ENCODING 170
+SWIDTH 549 0
+DWIDTH 12 0
+BBX 10 7 1 1
+BITMAP
+8800
+6600
+1980
+0440
+1980
+6600
+8800
+ENDCHAR
+STARTCHAR unionplus
+ENCODING 171
+SWIDTH 768 0
+DWIDTH 11 0
+BBX 9 8 1 1
+BITMAP
+8080
+8880
+8880
+be80
+8880
+8880
+4100
+3e00
+ENDCHAR
+STARTCHAR sqintersection
+ENCODING 172
+SWIDTH 768 0
+DWIDTH 11 0
+BBX 9 8 1 1
+BITMAP
+ff80
+8080
+8080
+8080
+8080
+8080
+8080
+8080
+ENDCHAR
+STARTCHAR squnion
+ENCODING 173
+SWIDTH 768 0
+DWIDTH 11 0
+BBX 9 8 1 1
+BITMAP
+8080
+8080
+8080
+8080
+8080
+8080
+8080
+ff80
+ENDCHAR
+STARTCHAR frown
+ENCODING 174
+SWIDTH 250 0
+DWIDTH 11 0
+BBX 9 3 1 3
+BITMAP
+3e00
+4100
+8080
+ENDCHAR
+STARTCHAR smile
+ENCODING 175
+SWIDTH 250 0
+DWIDTH 11 0
+BBX 9 3 1 3
+BITMAP
+8080
+4100
+3e00
+ENDCHAR
+STARTCHAR reflexprec
+ENCODING 176
+SWIDTH 549 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+02
+02
+0c
+f0
+0c
+02
+02
+00
+fe
+ENDCHAR
+STARTCHAR reflexsucc
+ENCODING 177
+SWIDTH 549 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+80
+80
+60
+1e
+60
+80
+80
+00
+fe
+ENDCHAR
+STARTCHAR properprec
+ENCODING 178
+SWIDTH 549 0
+DWIDTH 9 0
+BBX 7 7 1 1
+BITMAP
+02
+02
+0c
+f0
+0c
+02
+02
+ENDCHAR
+STARTCHAR propersucc
+ENCODING 179
+SWIDTH 549 0
+DWIDTH 9 0
+BBX 7 7 1 1
+BITMAP
+80
+80
+60
+1e
+60
+80
+80
+ENDCHAR
+STARTCHAR bardash
+ENCODING 180
+SWIDTH 494 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+80
+80
+80
+80
+fe
+80
+80
+80
+80
+ENDCHAR
+STARTCHAR dashbar
+ENCODING 181
+SWIDTH 494 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+02
+02
+02
+02
+fe
+02
+02
+02
+02
+ENDCHAR
+STARTCHAR bardashdbl
+ENCODING 182
+SWIDTH 494 0
+DWIDTH 9 0
+BBX 7 9 1 0
+BITMAP
+80
+80
+80
+fe
+80
+fe
+80
+80
+80
+ENDCHAR
+STARTCHAR smlintegral
+ENCODING 183
+SWIDTH 274 0
+DWIDTH 7 0
+BBX 5 10 1 0
+BITMAP
+18
+28
+20
+20
+20
+20
+20
+20
+a0
+c0
+ENDCHAR
+STARTCHAR circleintegral
+ENCODING 184
+SWIDTH 274 0
+DWIDTH 8 0
+BBX 6 13 1 -2
+BITMAP
+1c
+34
+30
+30
+78
+b4
+b4
+b4
+78
+30
+30
+b0
+e0
+ENDCHAR
+STARTCHAR coproduct
+ENCODING 185
+SWIDTH 823 0
+DWIDTH 12 0
+BBX 10 13 1 -2
+BITMAP
+f3c0
+6180
+6180
+6180
+6180
+6180
+6180
+6180
+6180
+6180
+6180
+6180
+ffc0
+ENDCHAR
+STARTCHAR bigcircledot
+ENCODING 186
+SWIDTH 768 0
+DWIDTH 13 0
+BBX 11 11 1 -1
+BITMAP
+1f00
+3f80
+71c0
+e0e0
+c060
+c460
+c060
+e0e0
+71c0
+3f80
+1f00
+ENDCHAR
+STARTCHAR bigcirclemultiply
+ENCODING 187
+SWIDTH 768 0
+DWIDTH 13 0
+BBX 11 11 1 -1
+BITMAP
+1f00
+3f80
+71c0
+f1e0
+ca60
+c460
+ca60
+f1e0
+71c0
+3f80
+1f00
+ENDCHAR
+STARTCHAR bigcircleplus
+ENCODING 188
+SWIDTH 768 0
+DWIDTH 13 0
+BBX 11 11 1 -1
+BITMAP
+1f00
+3f80
+75c0
+e4e0
+c460
+ffe0
+c460
+e4e0
+75c0
+3f80
+1f00
+ENDCHAR
+STARTCHAR biglogicaland
+ENCODING 189
+SWIDTH 603 0
+DWIDTH 13 0
+BBX 11 13 1 -2
+BITMAP
+0e00
+0e00
+1b00
+1b00
+1b00
+3180
+3180
+3180
+60c0
+60c0
+60c0
+c060
+c060
+ENDCHAR
+STARTCHAR biglogicalor
+ENCODING 190
+SWIDTH 603 0
+DWIDTH 13 0
+BBX 11 13 1 -2
+BITMAP
+c060
+c060
+60c0
+60c0
+60c0
+3180
+3180
+3180
+1b00
+1b00
+1b00
+0e00
+0e00
+ENDCHAR
+STARTCHAR bigintersection
+ENCODING 191
+SWIDTH 603 0
+DWIDTH 13 0
+BBX 11 13 1 -2
+BITMAP
+1f00
+3180
+60c0
+c060
+c060
+c060
+c060
+c060
+c060
+c060
+c060
+c060
+c060
+ENDCHAR
+STARTCHAR bigunion
+ENCODING 192
+SWIDTH 603 0
+DWIDTH 13 0
+BBX 11 13 1 -2
+BITMAP
+c060
+c060
+c060
+c060
+c060
+c060
+c060
+c060
+c060
+c060
+60c0
+3180
+1f00
+ENDCHAR
+STARTCHAR bigunionplus
+ENCODING 193
+SWIDTH 603 0
+DWIDTH 13 0
+BBX 11 13 1 -2
+BITMAP
+c060
+c060
+c060
+c060
+c460
+c460
+df60
+c460
+c460
+c060
+60c0
+3180
+1f00
+ENDCHAR
+STARTCHAR bigsqunion
+ENCODING 194
+SWIDTH 603 0
+DWIDTH 13 0
+BBX 11 13 1 -2
+BITMAP
+c060
+c060
+c060
+c060
+c060
+c060
+c060
+c060
+c060
+c060
+c060
+c060
+ffe0
+ENDCHAR
+STARTCHAR bigcircle
+ENCODING 195
+SWIDTH 768 0
+DWIDTH 12 0
+BBX 10 10 1 0
+BITMAP
+3f00
+6180
+c0c0
+8040
+8040
+8040
+8040
+c0c0
+6180
+3f00
+ENDCHAR
+STARTCHAR guilsinglleft
+ENCODING 196
+SWIDTH 250 0
+DWIDTH 5 0
+BBX 3 5 1 2
+BITMAP
+20
+40
+80
+40
+20
+ENDCHAR
+STARTCHAR circleminus
+ENCODING 197
+SWIDTH 768 0
+DWIDTH 11 0
+BBX 9 9 1 0
+BITMAP
+1c00
+6300
+4100
+8080
+ff80
+8080
+4100
+6300
+1c00
+ENDCHAR
+STARTCHAR smltriangleleft
+ENCODING 198
+SWIDTH 713 0
+DWIDTH 9 0
+BBX 7 7 1 1
+BITMAP
+06
+1a
+62
+c2
+62
+1a
+06
+ENDCHAR
+STARTCHAR perthousand
+ENCODING 199
+SWIDTH 1000 0
+DWIDTH 13 0
+BBX 11 11 1 0
+BITMAP
+0100
+6200
+9200
+9400
+6400
+0800
+1000
+16c0
+2920
+2920
+46c0
+ENDCHAR
+STARTCHAR existential1
+ENCODING 200
+SWIDTH 549 0
+DWIDTH 8 0
+BBX 6 10 1 0
+BITMAP
+fc
+04
+04
+04
+fc
+04
+04
+04
+04
+fc
+ENDCHAR
+STARTCHAR daggerdbl1
+ENCODING 201
+SWIDTH 250 0
+DWIDTH 7 0
+BBX 5 9 1 0
+BITMAP
+20
+f8
+20
+70
+20
+70
+20
+f8
+20
+ENDCHAR
+STARTCHAR daggerdbl
+ENCODING 202
+SWIDTH 250 0
+DWIDTH 7 0
+BBX 5 13 1 -2
+BITMAP
+20
+a8
+f8
+20
+70
+70
+20
+70
+70
+20
+f8
+a8
+20
+ENDCHAR
+STARTCHAR bigbowtie
+ENCODING 203
+SWIDTH 250 0
+DWIDTH 11 0
+BBX 9 9 1 0
+BITMAP
+8080
+c180
+a280
+9480
+8880
+9480
+a280
+c180
+8080
+ENDCHAR
+STARTCHAR circ
+ENCODING 204
+SWIDTH 460 0
+DWIDTH 7 0
+BBX 5 5 1 2
+BITMAP
+70
+88
+88
+88
+70
+ENDCHAR
+STARTCHAR grave
+ENCODING 205
+SWIDTH 333 0
+DWIDTH 4 0
+BBX 2 2 1 9
+BITMAP
+80
+40
+ENDCHAR
+STARTCHAR circumflex
+ENCODING 206
+SWIDTH 333 0
+DWIDTH 5 0
+BBX 3 2 1 9
+BITMAP
+40
+a0
+ENDCHAR
+STARTCHAR tilde
+ENCODING 207
+SWIDTH 333 0
+DWIDTH 7 0
+BBX 5 2 1 9
+BITMAP
+68
+b0
+ENDCHAR
+STARTCHAR longarrowboth
+ENCODING 208
+SWIDTH 987 0
+DWIDTH 21 0
+BBX 19 7 1 1
+BITMAP
+100100
+200080
+400040
+ffffe0
+400040
+200080
+100100
+ENDCHAR
+STARTCHAR endash
+ENCODING 209
+SWIDTH 556 0
+DWIDTH 9 0
+BBX 9 1 0 4
+BITMAP
+ff80
+ENDCHAR
+STARTCHAR emdash
+ENCODING 210
+SWIDTH 1000 0
+DWIDTH 16 0
+BBX 16 1 0 4
+BITMAP
+ffff
+ENDCHAR
+STARTCHAR Ydiaeresis
+ENCODING 211
+SWIDTH 667 0
+DWIDTH 9 0
+BBX 9 13 0 0
+BITMAP
+3600
+0000
+8080
+4100
+4100
+2200
+2200
+1400
+0800
+0800
+0800
+0800
+0800
+ENDCHAR
+STARTCHAR ampersand2
+ENCODING 212
+SWIDTH 778 0
+DWIDTH 11 0
+BBX 9 10 1 0
+BITMAP
+3000
+4800
+4800
+7000
+2700
+7200
+ca00
+8400
+ce80
+7b00
+ENDCHAR
+STARTCHAR universal1
+ENCODING 213
+SWIDTH 713 0
+DWIDTH 9 0
+BBX 9 10 0 0
+BITMAP
+8080
+4100
+4100
+3e00
+2200
+2200
+1400
+1400
+0800
+0800
+ENDCHAR
+STARTCHAR booleans
+ENCODING 214
+SWIDTH 667 0
+DWIDTH 11 0
+BBX 9 10 1 0
+BITMAP
+ff00
+5380
+5280
+5380
+5f00
+5380
+5280
+5280
+5380
+ff00
+ENDCHAR
+STARTCHAR complexnums
+ENCODING 215
+SWIDTH 722 0
+DWIDTH 10 0
+BBX 8 10 1 0
+BITMAP
+3d
+63
+a1
+a0
+a0
+a0
+a0
+a1
+63
+3e
+ENDCHAR
+STARTCHAR natnums
+ENCODING 216
+SWIDTH 722 0
+DWIDTH 11 0
+BBX 9 10 1 0
+BITMAP
+e380
+7100
+5900
+6d00
+7700
+5b00
+4d00
+4700
+4300
+e100
+ENDCHAR
+STARTCHAR rationalnums
+ENCODING 217
+SWIDTH 722 0
+DWIDTH 11 0
+BBX 9 11 1 -1
+BITMAP
+3e00
+6300
+a280
+a280
+a280
+a280
+a280
+a280
+6300
+3e00
+0780
+ENDCHAR
+STARTCHAR realnums
+ENCODING 218
+SWIDTH 667 0
+DWIDTH 11 0
+BBX 9 10 1 0
+BITMAP
+ff00
+5380
+5280
+5380
+5f00
+5a00
+5500
+5580
+5280
+f380
+ENDCHAR
+STARTCHAR integers
+ENCODING 219
+SWIDTH 611 0
+DWIDTH 10 0
+BBX 8 10 1 0
+BITMAP
+ff
+8a
+96
+34
+2c
+68
+58
+d3
+a5
+ff
+ENDCHAR
+STARTCHAR lesssim
+ENCODING 220
+SWIDTH 549 0
+DWIDTH 9 0
+BBX 7 10 1 0
+BITMAP
+02
+0c
+30
+c0
+30
+0c
+02
+00
+72
+9c
+ENDCHAR
+STARTCHAR greatersim
+ENCODING 221
+SWIDTH 549 0
+DWIDTH 9 0
+BBX 7 10 1 0
+BITMAP
+80
+60
+18
+06
+18
+60
+80
+00
+72
+9c
+ENDCHAR
+STARTCHAR lessapprox
+ENCODING 222
+SWIDTH 549 0
+DWIDTH 9 0
+BBX 7 13 1 -2
+BITMAP
+02
+0c
+30
+c0
+30
+0c
+02
+00
+72
+9c
+00
+72
+9c
+ENDCHAR
+STARTCHAR greaterapprox
+ENCODING 223
+SWIDTH 549 0
+DWIDTH 9 0
+BBX 7 13 1 -2
+BITMAP
+80
+60
+18
+06
+18
+60
+80
+00
+72
+9c
+00
+72
+9c
+ENDCHAR
+STARTCHAR definedas
+ENCODING 224
+SWIDTH 549 0
+DWIDTH 9 0
+BBX 7 7 1 2
+BITMAP
+10
+28
+7c
+00
+fe
+00
+fe
+ENDCHAR
+STARTCHAR circleminus1
+ENCODING 225
+SWIDTH 768 0
+DWIDTH 11 0
+BBX 9 9 1 0
+BITMAP
+1c00
+6300
+4100
+8080
+be80
+8080
+4100
+6300
+1c00
+ENDCHAR
+STARTCHAR circleasterisk
+ENCODING 226
+SWIDTH 768 0
+DWIDTH 11 0
+BBX 9 9 1 0
+BITMAP
+1c00
+6300
+4900
+aa80
+9c80
+aa80
+4900
+6300
+1c00
+ENDCHAR
+STARTCHAR circlecirc
+ENCODING 227
+SWIDTH 768 0
+DWIDTH 11 0
+BBX 9 9 1 0
+BITMAP
+1c00
+6300
+5d00
+a280
+a280
+a280
+5d00
+6300
+1c00
+ENDCHAR
+STARTCHAR dollar1
+ENCODING 228
+SWIDTH 556 0
+DWIDTH 9 0
+BBX 7 13 1 -2
+BITMAP
+28
+28
+7c
+aa
+a8
+a8
+7c
+2a
+2a
+aa
+7c
+28
+28
+ENDCHAR
+STARTCHAR euro
+ENCODING 229
+SWIDTH 722 0
+DWIDTH 11 0
+BBX 9 11 1 -1
+BITMAP
+1f00
+3180
+6080
+4000
+ff00
+4000
+fe00
+4000
+6080
+3180
+1f00
+ENDCHAR
+STARTCHAR therefore1
+ENCODING 230
+SWIDTH 863 0
+DWIDTH 10 0
+BBX 8 7 1 0
+BITMAP
+18
+18
+00
+00
+00
+c3
+c3
+ENDCHAR
+STARTCHAR coloncolon
+ENCODING 231
+SWIDTH 863 0
+DWIDTH 7 0
+BBX 5 7 1 0
+BITMAP
+d8
+d8
+00
+00
+00
+d8
+d8
+ENDCHAR
+STARTCHAR bigsqintersection
+ENCODING 232
+SWIDTH 603 0
+DWIDTH 13 0
+BBX 11 13 1 -2
+BITMAP
+ffe0
+c060
+c060
+c060
+c060
+c060
+c060
+c060
+c060
+c060
+c060
+c060
+c060
+ENDCHAR
+STARTCHAR semanticsleft
+ENCODING 233
+SWIDTH 556 0
+DWIDTH 6 0
+BBX 5 13 1 -2
+BITMAP
+f8
+a0
+a0
+a0
+a0
+a0
+a0
+a0
+a0
+a0
+a0
+a0
+f8
+ENDCHAR
+STARTCHAR semanticsright
+ENCODING 234
+SWIDTH 556 0
+DWIDTH 6 0
+BBX 5 13 0 -2
+BITMAP
+f8
+28
+28
+28
+28
+28
+28
+28
+28
+28
+28
+28
+f8
+ENDCHAR
+STARTCHAR doubleparenleft
+ENCODING 235
+SWIDTH 1000 0
+DWIDTH 6 0
+BBX 4 13 1 -2
+BITMAP
+30
+50
+50
+90
+90
+90
+90
+90
+90
+90
+50
+50
+30
+ENDCHAR
+STARTCHAR doubleparenright
+ENCODING 236
+SWIDTH 1000 0
+DWIDTH 6 0
+BBX 4 13 1 -2
+BITMAP
+c0
+a0
+a0
+90
+90
+90
+90
+90
+90
+90
+a0
+a0
+c0
+ENDCHAR
+ENDFONT
isabelle