more arrow symbols;

--- a/NEWS	Tue Dec 29 19:11:23 2015 +0100
+++ b/NEWS	Tue Dec 29 20:58:18 2015 +0100
@@ -31,6 +31,18 @@
 remains available under print mode "ASCII", but less important syntax
 has been removed (see below).
 
+* Support for arrows of various lengths, with rendering in LaTeX and
+Isabelle fonts:
+
+  \<leftarrow>
+  \<longleftarrow>
+  \<longlongleftarrow>
+  \<longlonglongleftarrow>
+  \<rightarrow>
+  \<longrightarrow>
+  \<longlongrightarrow>
+  \<longlonglongrightarrow>
+
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 

--- a/etc/abbrevs	Tue Dec 29 19:11:23 2015 +0100
+++ b/etc/abbrevs	Tue Dec 29 20:58:18 2015 +0100
@@ -1,5 +1,5 @@
 (* additional abbreviations for syntactic completion *)
 
 (*prevent replacement of very long arrows*)
-"--->" = "--->"
+"----->" = "----->"
 "===>" = "===>"

--- a/etc/symbols	Tue Dec 29 19:11:23 2015 +0100
+++ b/etc/symbols	Tue Dec 29 20:58:18 2015 +0100
@@ -156,8 +156,12 @@
 \<int>                  code: 0x002124  group: letter
 \<leftarrow>            code: 0x002190  group: arrow  abbrev: <.
 \<longleftarrow>        code: 0x0027f5  group: arrow  abbrev: <.
+\<longlongleftarrow>    code: 0x00290e  group: arrow  abbrev: <.
+\<longlonglongleftarrow> code: 0x0021e0 group: arrow  abbrev: <.
 \<rightarrow>           code: 0x002192  group: arrow  abbrev: .>  abbrev: ->
 \<longrightarrow>       code: 0x0027f6  group: arrow  abbrev: .>  abbrev: -->
+\<longlongrightarrow>   code: 0x00290f  group: arrow  abbrev: .>  abbrev: --->
+\<longlonglongrightarrow> code: 0x0021e2 group: arrow abbrev: .>  abbrev: ---->
 \<Leftarrow>            code: 0x0021d0  group: arrow  abbrev: <.
 \<Longleftarrow>        code: 0x0027f8  group: arrow  abbrev: <.
 \<Rightarrow>           code: 0x0021d2  group: arrow  abbrev: .>  abbrev: =>

--- a/lib/fonts/IsabelleText.sfd	Tue Dec 29 19:11:23 2015 +0100
+++ b/lib/fonts/IsabelleText.sfd	Tue Dec 29 20:58:18 2015 +0100
@@ -19,7 +19,7 @@
 OS2_WeightWidthSlopeOnly: 0
 OS2_UseTypoMetrics: 1
 CreationTime: 1050361371
-ModificationTime: 1446896286
+ModificationTime: 1451417325
 PfmFamily: 17
 TTFWeight: 400
 TTFWidth: 5
@@ -2241,11 +2241,11 @@
 DisplaySize: -96
 AntiAlias: 1
 FitToEm: 1
-WinInfo: 9864 18 16
+WinInfo: 10278 18 16
 BeginPrivate: 0
 EndPrivate
 TeXData: 1 0 0 631296 315648 210432 572416 -1048576 210432 783286 444596 497025 792723 393216 433062 380633 303038 157286 324010 404750 52429 2506097 1059062 262144
-BeginChars: 1114189 1398
+BeginChars: 1114189 1399
 
 StartChar: u10000
 Encoding: 65536 65536 0
@@ -54601,34 +54601,68 @@
 
 StartChar: uni21E0
 Encoding: 8672 8672 1077
-Width: 1233
-Flags: W
-LayerCount: 2
-Fore
-SplineSet
-545 643 m 1,0,-1
- 545.001 478.998 l 1,1,-1
- 287 479 l 9,2,-1
- 447 319 l 1,3,-1
- 357 229 l 1,4,-1
- 66 520 l 9,5,-1
- 66 602 l 17,6,-1
- 357 893 l 1,7,-1
- 447 803 l 1,8,-1
- 287 643 l 17,9,-1
- 545 643 l 1,0,-1
-670.001 479.001 m 1,10,-1
- 670 642.999 l 1,11,-1
- 856.999 643 l 1,12,-1
- 856.999 478.998 l 1,13,-1
- 670.001 479.001 l 1,10,-1
-980.001 479.001 m 1,14,-1
- 980.001 642.997 l 1,15,-1
- 1167 643 l 1,16,-1
- 1167 479 l 1,17,-1
- 980.001 479.001 l 1,14,-1
-EndSplineSet
-Validated: 1
+Width: 6063
+VWidth: 2220
+Flags: W
+HStem: 511 88<394 5848.81>
+VStem: 563 71<166.706 257.064>
+LayerCount: 2
+Fore
+SplineSet
+5782 511.5 m 6,0,-1
+ 2172 511 l 2,1,2
+ 2147.74 511.152 l 0,3,4
+ 2137.01 511.244 l 1,5,6
+ 2122 511 l 2,7,-1
+ 2101 511 l 1,8,-1
+ 394 511 l 1,9,10
+ 452 469 452 469 501 412 c 128,-1,11
+ 550 355 550 355 577 308 c 128,-1,12
+ 604 261 604 261 619 228 c 128,-1,13
+ 634 195 634 195 634 186 c 0,14,15
+ 634 172 634 172 624 166 c 128,-1,16
+ 614 160 614 160 601 160 c 0,17,18
+ 584 160 584 160 577.5 166.5 c 128,-1,19
+ 571 173 571 173 563 191 c 0,20,21
+ 512 301 512 301 437 383.5 c 0,22,23
+ 368.667 458.667 368.667 458.667 234 526 c 0,24,25
+ 228 529 228 529 223.5 532 c 128,-1,26
+ 219 535 219 535 215.5 538 c 128,-1,27
+ 212 541 212 541 210 545 c 128,-1,28
+ 208 549 208 549 208 555 c 128,-1,29
+ 208 561 208 561 208.5 564 c 128,-1,30
+ 209 567 209 567 215 571.5 c 128,-1,31
+ 221 576 221 576 222.5 577 c 128,-1,32
+ 224 578 224 578 239 586 c 0,33,34
+ 302 616 302 616 355 655.5 c 128,-1,35
+ 408 695 408 695 440 728 c 0,36,37
+ 472 762 472 762 500 805 c 0,38,39
+ 531.719 853.711 531.719 853.711 539.5 871.5 c 0,40,41
+ 558.722 915.443 558.722 915.443 565 928 c 0,42,43
+ 569 936 569 936 570.5 938.5 c 128,-1,44
+ 572 941 572 941 580 945.5 c 128,-1,45
+ 588 950 588 950 601 950 c 0,46,47
+ 615 950 615 950 624.5 943.5 c 128,-1,48
+ 634 937 634 937 634 924 c 0,49,50
+ 634 915 634 915 619 882 c 128,-1,51
+ 604 849 604 849 577 802 c 128,-1,52
+ 550 755 550 755 501 698.5 c 128,-1,53
+ 452 642 452 642 394 599 c 1,54,-1
+ 2101 599 l 1,55,-1
+ 2122 599 l 2,56,57
+ 2136.92 598.968 l 1,58,59
+ 2148.11 598.97 l 0,60,-1
+ 2172 599 l 2,61,-1
+ 5782 599.5 l 6,62,63
+ 5797.84 599.502 5797.84 599.502 5807.5 599 c 132,-1,64
+ 5817 598.5 5817 598.5 5830 594.5 c 132,-1,65
+ 5843 590.5 5843 590.5 5849 581 c 132,-1,66
+ 5855 571.5 5855 571.5 5855 555.5 c 132,-1,67
+ 5855 539.5 5855 539.5 5849 530 c 132,-1,68
+ 5843 520.5 5843 520.5 5830 516.5 c 132,-1,69
+ 5817 512.5 5817 512.5 5807.5 512 c 4,70,71
+ 5798.64 511.502 5798.64 511.502 5782 511.5 c 6,0,-1
+EndSplineSet
 EndChar
 
 StartChar: uni21E1
@@ -54665,34 +54699,68 @@
 
 StartChar: uni21E2
 Encoding: 8674 8674 1079
-Width: 1233
-Flags: W
-LayerCount: 2
-Fore
-SplineSet
-688 643 m 1,0,-1
- 946 643 l 9,1,-1
- 786 803 l 1,2,-1
- 876 893 l 1,3,-1
- 1167 602 l 9,4,-1
- 1167 520 l 17,5,-1
- 876 229 l 1,6,-1
- 786 319 l 1,7,-1
- 946 479 l 17,8,-1
- 687.999 478.998 l 1,9,-1
- 688 643 l 1,0,-1
-562.999 479.001 m 1,10,-1
- 376.001 478.998 l 1,11,-1
- 376.001 643 l 1,12,-1
- 563 642.999 l 1,13,-1
- 562.999 479.001 l 1,10,-1
-252.999 479.001 m 1,14,-1
- 66 479 l 1,15,-1
- 66 643 l 1,16,-1
- 252.999 642.997 l 1,17,-1
- 252.999 479.001 l 1,14,-1
-EndSplineSet
-Validated: 1
+Width: 6062
+VWidth: 2220
+Flags: W
+HStem: 511.5 88<218.705 5664>
+VStem: 5424 71<849.469 944.029>
+LayerCount: 2
+Fore
+SplineSet
+2694 511.5 m 2,0,-1
+ 285 511 l 2,1,2
+ 269.114 510.997 269.114 510.997 260 511.5 c 128,-1,3
+ 251 512 251 512 238 516 c 128,-1,4
+ 225 520 225 520 218.5 529.5 c 128,-1,5
+ 212 539 212 539 212 555 c 128,-1,6
+ 212 571 212 571 218.5 580.5 c 128,-1,7
+ 225 590 225 590 238 594 c 128,-1,8
+ 251 598 251 598 260 598.5 c 128,-1,9
+ 268.974 598.997 268.974 598.997 285 599 c 2,10,-1
+ 2694 599.5 l 2,11,12
+ 2713.46 599.458 l 0,13,-1
+ 2724.83 599.208 l 0,14,15
+ 2735 599.5 l 2,16,-1
+ 2756 599.5 l 1,17,-1
+ 5664 599.25 l 5,18,19
+ 5606 641.25 5606 641.25 5556.5 698.25 c 132,-1,20
+ 5507 755.25 5507 755.25 5480 802.25 c 132,-1,21
+ 5453 849.25 5453 849.25 5438.5 882.25 c 132,-1,22
+ 5424 915.25 5424 915.25 5424 924.25 c 4,23,24
+ 5424 938.25 5424 938.25 5434 944.25 c 132,-1,25
+ 5444 950.25 5444 950.25 5457 950.25 c 4,26,27
+ 5474 950.25 5474 950.25 5481 944.25 c 4,28,29
+ 5487 937.25 5487 937.25 5495 919.25 c 4,30,31
+ 5526 848.25 5526 848.25 5569 788.25 c 4,32,33
+ 5609 731.25 5609 731.25 5655 691.75 c 132,-1,34
+ 5701 652.25 5701 652.25 5742 626.75 c 132,-1,35
+ 5783 601.25 5783 601.25 5834 577.25 c 5,36,37
+ 5837 577.25 5837 577.25 5843.5 571.25 c 132,-1,38
+ 5850 565.25 5850 565.25 5850 555.25 c 4,39,40
+ 5850 544.25 5850 544.25 5845 539.25 c 132,-1,41
+ 5840 534.25 5840 534.25 5819 524.25 c 4,42,43
+ 5773 502.25 5773 502.25 5732.5 475.75 c 132,-1,44
+ 5692 449.25 5692 449.25 5663 424.75 c 132,-1,45
+ 5634 400.25 5634 400.25 5607.5 369.25 c 132,-1,46
+ 5581 338.25 5581 338.25 5565 316.25 c 132,-1,47
+ 5549 294.25 5549 294.25 5532.5 264.25 c 4,48,49
+ 5511.31 225.717 5511.31 225.717 5509.5 220.25 c 4,50,51
+ 5504.63 205.505 5504.63 205.505 5493 182.25 c 4,52,53
+ 5489 174.25 5489 174.25 5487 171.75 c 132,-1,54
+ 5485 169.25 5485 169.25 5477 164.25 c 4,55,56
+ 5469 160.25 5469 160.25 5457 160.25 c 4,57,58
+ 5443 160.25 5443 160.25 5433.5 166.75 c 132,-1,59
+ 5424 173.25 5424 173.25 5424 186.25 c 4,60,61
+ 5424 195.25 5424 195.25 5438.5 228.25 c 132,-1,62
+ 5453 261.25 5453 261.25 5480 308.25 c 132,-1,63
+ 5507 355.25 5507 355.25 5556.5 412.25 c 132,-1,64
+ 5606 469.25 5606 469.25 5664 511.25 c 5,65,-1
+ 2756 511.5 l 1,66,-1
+ 2735 511.5 l 2,67,68
+ 2725.08 511.875 l 0,69,70
+ 2715.96 511.875 l 0,71,-1
+ 2694 511.5 l 2,0,-1
+EndSplineSet
 EndChar
 
 StartChar: uni21E3
@@ -62017,7 +62085,7 @@
 EndChar
 
 StartChar: uni2756
-Encoding: 10070 10070 1397
+Encoding: 10070 10070 1396
 Width: 1233
 Flags: W
 LayerCount: 2
@@ -62045,5 +62113,137 @@
  358 254 l 1,12,-1
 EndSplineSet
 EndChar
+
+StartChar: uni290E
+Encoding: 10510 10510 1397
+Width: 4863
+VWidth: 2220
+Flags: W
+HStem: 511 88<394 4648.81>
+VStem: 563 71<166.706 257.064>
+LayerCount: 2
+Fore
+SplineSet
+4582 511.5 m 2,0,-1
+ 2172 511 l 2,1,2
+ 2147.74 511.152 l 0,3,4
+ 2137.01 511.244 l 1,5,6
+ 2122 511 l 2,7,-1
+ 2101 511 l 1,8,-1
+ 394 511 l 1,9,10
+ 452 469 452 469 501 412 c 128,-1,11
+ 550 355 550 355 577 308 c 128,-1,12
+ 604 261 604 261 619 228 c 128,-1,13
+ 634 195 634 195 634 186 c 0,14,15
+ 634 172 634 172 624 166 c 128,-1,16
+ 614 160 614 160 601 160 c 0,17,18
+ 584 160 584 160 577.5 166.5 c 128,-1,19
+ 571 173 571 173 563 191 c 0,20,21
+ 512 301 512 301 437 383.5 c 0,22,23
+ 368.667 458.667 368.667 458.667 234 526 c 0,24,25
+ 228 529 228 529 223.5 532 c 128,-1,26
+ 219 535 219 535 215.5 538 c 128,-1,27
+ 212 541 212 541 210 545 c 128,-1,28
+ 208 549 208 549 208 555 c 128,-1,29
+ 208 561 208 561 208.5 564 c 128,-1,30
+ 209 567 209 567 215 571.5 c 128,-1,31
+ 221 576 221 576 222.5 577 c 128,-1,32
+ 224 578 224 578 239 586 c 0,33,34
+ 302 616 302 616 355 655.5 c 128,-1,35
+ 408 695 408 695 440 728 c 0,36,37
+ 472 762 472 762 500 805 c 0,38,39
+ 531.719 853.711 531.719 853.711 539.5 871.5 c 0,40,41
+ 558.722 915.443 558.722 915.443 565 928 c 0,42,43
+ 569 936 569 936 570.5 938.5 c 128,-1,44
+ 572 941 572 941 580 945.5 c 128,-1,45
+ 588 950 588 950 601 950 c 0,46,47
+ 615 950 615 950 624.5 943.5 c 128,-1,48
+ 634 937 634 937 634 924 c 0,49,50
+ 634 915 634 915 619 882 c 128,-1,51
+ 604 849 604 849 577 802 c 128,-1,52
+ 550 755 550 755 501 698.5 c 128,-1,53
+ 452 642 452 642 394 599 c 1,54,-1
+ 2101 599 l 1,55,-1
+ 2122 599 l 2,56,57
+ 2136.92 598.968 l 1,58,59
+ 2148.11 598.97 l 0,60,-1
+ 2172 599 l 2,61,-1
+ 4582 599.5 l 2,62,63
+ 4597.93 599.503 4597.93 599.503 4607.5 599 c 128,-1,64
+ 4617 598.5 4617 598.5 4630 594.5 c 128,-1,65
+ 4643 590.5 4643 590.5 4649 581 c 128,-1,66
+ 4655 571.5 4655 571.5 4655 555.5 c 128,-1,67
+ 4655 539.5 4655 539.5 4649 530 c 128,-1,68
+ 4643 520.5 4643 520.5 4630 516.5 c 128,-1,69
+ 4617 512.5 4617 512.5 4607.5 512 c 0,70,71
+ 4598.38 511.503 4598.38 511.503 4582 511.5 c 2,0,-1
+EndSplineSet
+EndChar
+
+StartChar: uni290F
+Encoding: 10511 10511 1398
+Width: 4862
+VWidth: 2220
+Flags: W
+HStem: 511 88<218.705 4464>
+VStem: 4224 71<849.719 944.279>
+LayerCount: 2
+Fore
+SplineSet
+2694 511.5 m 6,0,-1
+ 285 511 l 2,1,2
+ 269.087 510.997 269.087 510.997 260 511.5 c 128,-1,3
+ 251 512 251 512 238 516 c 128,-1,4
+ 225 520 225 520 218.5 529.5 c 128,-1,5
+ 212 539 212 539 212 555 c 128,-1,6
+ 212 571 212 571 218.5 580.5 c 128,-1,7
+ 225 590 225 590 238 594 c 128,-1,8
+ 251 598 251 598 260 598.5 c 128,-1,9
+ 268.974 598.997 268.974 598.997 285 599 c 2,10,-1
+ 2694 599.5 l 2,11,12
+ 2713.46 599.458 l 0,13,-1
+ 2724.83 599.208 l 0,14,15
+ 2735 599.5 l 2,16,-1
+ 2756 599.5 l 1,17,-1
+ 4464 599.5 l 1,18,19
+ 4406 641.5 4406 641.5 4356.5 698.5 c 128,-1,20
+ 4307 755.5 4307 755.5 4280 802.5 c 128,-1,21
+ 4253 849.5 4253 849.5 4238.5 882.5 c 128,-1,22
+ 4224 915.5 4224 915.5 4224 924.5 c 0,23,24
+ 4224 938.5 4224 938.5 4234 944.5 c 128,-1,25
+ 4244 950.5 4244 950.5 4257 950.5 c 0,26,27
+ 4274 950.5 4274 950.5 4281 944.5 c 0,28,29
+ 4287 937.5 4287 937.5 4295 919.5 c 0,30,31
+ 4326 848.5 4326 848.5 4369 788.5 c 0,32,33
+ 4409 731.5 4409 731.5 4455 692 c 128,-1,34
+ 4501 652.5 4501 652.5 4542 627 c 128,-1,35
+ 4583 601.5 4583 601.5 4634 577.5 c 1,36,37
+ 4637 577.5 4637 577.5 4643.5 571.5 c 128,-1,38
+ 4650 565.5 4650 565.5 4650 555.5 c 0,39,40
+ 4650 544.5 4650 544.5 4645 539.5 c 128,-1,41
+ 4640 534.5 4640 534.5 4619 524.5 c 0,42,43
+ 4573 502.5 4573 502.5 4532.5 476 c 128,-1,44
+ 4492 449.5 4492 449.5 4463 425 c 128,-1,45
+ 4434 400.5 4434 400.5 4407.5 369.5 c 128,-1,46
+ 4381 338.5 4381 338.5 4365 316.5 c 128,-1,47
+ 4349 294.5 4349 294.5 4332.5 264.5 c 0,48,49
+ 4311.31 225.967 4311.31 225.967 4309.5 220.5 c 0,50,51
+ 4304.63 205.755 4304.63 205.755 4293 182.5 c 0,52,53
+ 4289 174.5 4289 174.5 4287 172 c 128,-1,54
+ 4285 169.5 4285 169.5 4277 164.5 c 0,55,56
+ 4269 160.5 4269 160.5 4257 160.5 c 0,57,58
+ 4243 160.5 4243 160.5 4233.5 167 c 128,-1,59
+ 4224 173.5 4224 173.5 4224 186.5 c 0,60,61
+ 4224 195.5 4224 195.5 4238.5 228.5 c 128,-1,62
+ 4253 261.5 4253 261.5 4280 308.5 c 128,-1,63
+ 4307 355.5 4307 355.5 4356.5 412.5 c 128,-1,64
+ 4406 469.5 4406 469.5 4464 511.5 c 1,65,-1
+ 2756 511.5 l 5,66,-1
+ 2735 511.5 l 6,67,68
+ 2725.08 511.875 l 4,69,70
+ 2715.96 511.875 l 4,71,-1
+ 2694 511.5 l 6,0,-1
+EndSplineSet
+EndChar
 EndChars
 EndSplineFont

--- a/lib/fonts/IsabelleTextBold.sfd	Tue Dec 29 19:11:23 2015 +0100
+++ b/lib/fonts/IsabelleTextBold.sfd	Tue Dec 29 20:58:18 2015 +0100
@@ -20,7 +20,7 @@
 OS2_WeightWidthSlopeOnly: 0
 OS2_UseTypoMetrics: 1
 CreationTime: 1050374980
-ModificationTime: 1446896348
+ModificationTime: 1451417467
 PfmFamily: 17
 TTFWeight: 700
 TTFWidth: 5
@@ -1678,10 +1678,10 @@
 DisplaySize: -96
 AntiAlias: 1
 FitToEm: 1
-WinInfo: 9996 21 15
+WinInfo: 8568 21 15
 BeginPrivate: 0
 EndPrivate
-BeginChars: 1114115 1389
+BeginChars: 1114115 1391
 
 StartChar: .notdef
 Encoding: 1114112 -1 0
@@ -48157,32 +48157,83 @@
 
 StartChar: uni21E0
 Encoding: 8672 8672 1077
-Width: 1233
-Flags: W
-LayerCount: 2
-Fore
-SplineSet
-545 673 m 1,0,-1
- 545 449 l 1,1,-1
- 347 449 l 1,2,-1
- 477 319 l 1,3,-1
- 357 199 l 1,4,-1
- 66 490 l 1,5,-1
- 66 632 l 1,6,-1
- 357 923 l 1,7,-1
- 477 803 l 1,8,-1
- 347 673 l 1,9,-1
- 545 673 l 1,0,-1
-670 449 m 1,10,-1
- 670 673 l 1,11,-1
- 857 673 l 1,12,-1
- 857 449 l 1,13,-1
- 670 449 l 1,10,-1
-980 449 m 1,14,-1
- 980 673 l 1,15,-1
- 1167 673 l 1,16,-1
- 1167 449 l 1,17,-1
- 980 449 l 1,14,-1
+Width: 6063
+VWidth: 2220
+Flags: W
+HStem: 460 190<526.64 5893.39>
+LayerCount: 2
+Fore
+SplineSet
+5782.01 460.5 m 2,0,-1
+ 2171.84 460 l 1,1,-1
+ 2147.36 460.154 l 1,2,-1
+ 2137.21 460.241 l 1,3,-1
+ 2122.41 460 l 1,4,-1
+ 526.64 460 l 1,5,6
+ 533.536 452.388 533.536 452.388 539.674 445.246 c 0,7,8
+ 591.818 384.59 591.818 384.59 621.222 333.404 c 0,9,10
+ 649.427 284.306 649.427 284.306 665.429 249.104 c 0,11,12
+ 667.284 245.025 667.284 245.025 671.437 236.4 c 128,-1,13
+ 675.589 227.776 675.589 227.776 677.162 223.965 c 128,-1,14
+ 678.735 220.155 678.735 220.155 681.046 213.392 c 128,-1,15
+ 683.357 206.629 683.357 206.629 684.178 200.206 c 128,-1,16
+ 685 193.783 685 193.783 685 186 c 0,17,18
+ 685 168.111 685 168.111 676.078 150.264 c 128,-1,19
+ 667.155 132.417 667.155 132.417 650.239 122.268 c 0,20,21
+ 628.126 109 628.126 109 601 109 c 0,22,23
+ 562.875 109 562.875 109 541.438 130.438 c 0,24,25
+ 528.24 143.635 528.24 143.635 516.561 169.916 c 0,26,27
+ 469.006 272.477 469.006 272.477 399.263 349.194 c 0,28,29
+ 337.335 417.314 337.335 417.314 211.192 480.384 c 0,30,31
+ 202.353 484.803 202.353 484.803 195.21 489.565 c 128,-1,32
+ 188.149 494.273 188.149 494.273 182.31 499.278 c 0,33,34
+ 170.991 508.98 170.991 508.98 164.384 522.192 c 0,35,36
+ 157 536.96 157 536.96 157 555 c 0,37,38
+ 157 565.221 157 565.221 158.194 572.384 c 0,39,40
+ 159.313 579.101 159.313 579.101 161.486 584.891 c 128,-1,41
+ 163.659 590.682 163.659 590.682 165.713 594.27 c 128,-1,42
+ 167.767 597.858 167.767 597.858 171.056 601.384 c 128,-1,43
+ 174.346 604.91 174.346 604.91 176.034 606.284 c 128,-1,44
+ 177.722 607.658 177.722 607.658 180.939 609.888 c 128,-1,45
+ 184.156 612.117 184.156 612.117 184.4 612.3 c 0,46,47
+ 191.536 617.651 191.536 617.651 194.21 619.435 c 0,48,49
+ 197.794 621.824 197.794 621.824 215 631 c 2,50,-1
+ 216.025 631.547 l 1,51,-1
+ 217.073 632.046 l 2,52,53
+ 275.547 659.891 275.547 659.891 324.524 696.392 c 0,54,55
+ 373.814 733.128 373.814 733.128 403.127 763.236 c 0,56,57
+ 432.003 794.039 432.003 794.039 457.262 832.829 c 0,58,59
+ 486.682 878.009 486.682 878.009 492.775 891.939 c 0,60,61
+ 512.518 937.077 512.518 937.077 519.384 950.808 c 0,62,63
+ 524.259 960.558 524.259 960.558 526.768 964.739 c 0,64,65
+ 531.023 971.832 531.023 971.832 535.597 976.772 c 128,-1,66
+ 540.171 981.711 540.171 981.711 542.525 983.359 c 128,-1,67
+ 544.879 985.007 544.879 985.007 549.608 987.293 c 128,-1,68
+ 554.336 989.579 554.336 989.579 554.997 989.95 c 0,69,70
+ 574.642 1001 574.642 1001 601 1001 c 0,71,72
+ 630.778 1001 630.778 1001 653.299 985.591 c 0,73,74
+ 685 963.9 685 963.9 685 924 c 0,75,76
+ 685 916.203 685 916.203 684.179 909.776 c 128,-1,77
+ 683.357 903.348 683.357 903.348 681.052 896.6 c 128,-1,78
+ 678.746 889.851 678.746 889.851 677.167 886.032 c 128,-1,79
+ 675.589 882.212 675.589 882.212 671.444 873.611 c 128,-1,80
+ 667.298 865.01 667.298 865.01 665.429 860.896 c 0,81,82
+ 649.428 825.698 649.428 825.698 621.222 776.596 c 0,83,84
+ 591.768 725.32 591.768 725.32 539.529 665.086 c 0,85,86
+ 533.058 657.623 533.058 657.623 526.091 650 c 1,87,-1
+ 2122.05 650 l 1,88,-1
+ 2136.97 649.968 l 1,89,-1
+ 2148.09 649.97 l 1,90,-1
+ 2171.98 650 l 1,91,-1
+ 5781.99 650.5 l 2,92,93
+ 5799.17 650.502 5799.17 650.502 5810.19 649.929 c 0,94,95
+ 5825.98 649.098 5825.98 649.098 5845 643.245 c 0,96,97
+ 5876.03 633.694 5876.03 633.694 5892.12 608.234 c 0,98,99
+ 5906 586.265 5906 586.265 5906 555.5 c 128,-1,100
+ 5906 524.735 5906 524.735 5892.12 502.766 c 0,101,102
+ 5876.03 477.308 5876.03 477.308 5845 467.755 c 0,103,104
+ 5825.98 461.902 5825.98 461.902 5810.27 461.075 c 0,105,106
+ 5800.07 460.503 5800.07 460.503 5782.01 460.5 c 2,0,-1
 EndSplineSet
 EndChar
 
@@ -48219,32 +48270,76 @@
 
 StartChar: uni21E2
 Encoding: 8674 8674 1079
-Width: 1233
-Flags: W
-LayerCount: 2
-Fore
-SplineSet
-688 673 m 1,0,-1
- 886 673 l 1,1,-1
- 756 803 l 1,2,-1
- 876 923 l 1,3,-1
- 1167 632 l 1,4,-1
- 1167 490 l 1,5,-1
- 876 199 l 1,6,-1
- 756 319 l 1,7,-1
- 886 449 l 1,8,-1
- 688 449 l 1,9,-1
- 688 673 l 1,0,-1
-563 449 m 1,10,-1
- 376 449 l 1,11,-1
- 376 673 l 1,12,-1
- 563 673 l 1,13,-1
- 563 449 l 1,10,-1
-253 449 m 1,14,-1
- 66 449 l 1,15,-1
- 66 673 l 1,16,-1
- 253 673 l 1,17,-1
- 253 449 l 1,14,-1
+Width: 6062
+VWidth: 2220
+Flags: W
+HStem: 460.5 190<174.096 5530.96>
+LayerCount: 2
+Fore
+SplineSet
+5855.56 623.662 m 0,0,1
+ 5867.07 618.897 5867.07 618.897 5878.09 608.726 c 0,2,3
+ 5901 587.581 5901 587.581 5901 555.25 c 0,4,5
+ 5901 523.127 5901 523.127 5881.06 503.188 c 0,6,7
+ 5869.86 491.98 5869.86 491.98 5840.97 478.223 c 0,8,9
+ 5798.13 457.739 5798.13 457.739 5760.42 433.074 c 128,-1,10
+ 5722.52 408.279 5722.52 408.279 5695.91 385.792 c 0,11,12
+ 5670.09 363.974 5670.09 363.974 5646.25 336.111 c 0,13,14
+ 5621.13 306.707 5621.13 306.707 5606.25 286.253 c 0,15,16
+ 5592.15 266.881 5592.15 266.881 5577.19 239.672 c 0,17,18
+ 5561.46 211.073 5561.46 211.073 5557.28 202.326 c 1,19,20
+ 5551.19 184.575 5551.19 184.575 5538.62 159.442 c 0,21,22
+ 5532.2 146.614 5532.2 146.614 5526.82 139.891 c 0,23,24
+ 5519.4 130.606 5519.4 130.606 5504.03 121.002 c 2,25,-1
+ 5499.81 118.634 l 2,26,27
+ 5481.04 109.25 5481.04 109.25 5457 109.25 c 0,28,29
+ 5427.22 109.25 5427.22 109.25 5404.7 124.659 c 0,30,31
+ 5373 146.352 5373 146.352 5373 186.25 c 0,32,33
+ 5373 193.878 5373 193.878 5373.77 200.169 c 128,-1,34
+ 5374.55 206.46 5374.55 206.46 5376.78 213.179 c 128,-1,35
+ 5379 219.899 5379 219.899 5380.48 223.633 c 128,-1,36
+ 5381.96 227.367 5381.96 227.367 5386 236.044 c 128,-1,37
+ 5390.04 244.722 5390.04 244.722 5391.81 248.766 c 0,38,39
+ 5407.41 284.269 5407.41 284.269 5435.78 333.654 c 0,40,41
+ 5465.25 384.958 5465.25 384.958 5517.99 445.69 c 0,42,43
+ 5524.23 452.878 5524.23 452.878 5530.99 460.261 c 1,44,-1
+ 2734.04 460.5 l 1,45,-1
+ 2724.12 460.875 l 1,46,-1
+ 2716.39 460.875 l 1,47,-1
+ 2694.44 460.5 l 1,48,-1
+ 285.011 460 l 2,49,50
+ 267.713 459.996 267.713 459.996 257.171 460.579 c 0,51,52
+ 241.952 461.424 241.952 461.424 223.002 467.255 c 0,53,54
+ 192.97 476.496 192.97 476.496 176.409 500.701 c 0,55,56
+ 161 523.223 161 523.223 161 555 c 128,-1,57
+ 161 586.777 161 586.777 176.409 609.299 c 0,58,59
+ 192.971 633.505 192.971 633.505 223.002 642.745 c 0,60,61
+ 241.954 648.576 241.954 648.576 257.181 649.422 c 0,62,63
+ 267.571 649.997 267.571 649.997 284.989 650 c 2,64,-1
+ 2694.05 650.5 l 1,65,-1
+ 2714.07 650.457 l 1,66,-1
+ 2724.66 650.224 l 1,67,-1
+ 2734.27 650.5 l 1,68,-1
+ 5530.96 650.261 l 1,69,70
+ 5524.24 657.616 5524.24 657.616 5517.99 664.81 c 0,71,72
+ 5465.25 725.541 5465.25 725.541 5435.78 776.846 c 0,73,74
+ 5407.41 826.241 5407.41 826.241 5391.81 861.734 c 0,75,76
+ 5390.06 865.726 5390.06 865.726 5386.01 874.44 c 128,-1,77
+ 5381.96 883.154 5381.96 883.154 5380.49 886.873 c 128,-1,78
+ 5379.02 890.591 5379.02 890.591 5376.78 897.332 c 128,-1,79
+ 5374.55 904.072 5374.55 904.072 5373.78 910.357 c 128,-1,80
+ 5373 916.642 5373 916.642 5373 924.25 c 0,81,82
+ 5373 942.139 5373 942.139 5381.92 959.986 c 128,-1,83
+ 5390.85 977.833 5390.85 977.833 5407.76 987.982 c 0,84,85
+ 5429.87 1001.25 5429.87 1001.25 5457 1001.25 c 0,86,87
+ 5492.87 1001.25 5492.87 1001.25 5514.19 982.972 c 2,88,-1
+ 5517.17 980.419 l 1,89,-1
+ 5519.72 977.44 l 2,90,91
+ 5530.57 964.788 5530.57 964.788 5541.67 939.806 c 0,92,93
+ 5570.54 873.646 5570.54 873.646 5610.61 817.737 c 0,94,95
+ 5647.05 765.794 5647.05 765.794 5688.23 730.442 c 0,96,97
+ 5731.27 693.483 5731.27 693.483 5768.94 670.057 c 0,98,99
+ 5806.14 646.919 5806.14 646.919 5855.56 623.662 c 0,0,1
 EndSplineSet
 EndChar
 
@@ -68287,5 +68382,162 @@
  358 254 l 1,12,-1
 EndSplineSet
 EndChar
+
+StartChar: uni290E
+Encoding: 10510 10510 1389
+Width: 4863
+VWidth: 2220
+Flags: W
+HStem: 460 190<526.64 4693.39>
+LayerCount: 2
+Fore
+SplineSet
+4582.01 460.5 m 2,0,-1
+ 2171.85 460 l 1,1,-1
+ 2147.36 460.154 l 1,2,-1
+ 2137.21 460.241 l 1,3,-1
+ 2122.41 460 l 1,4,-1
+ 526.64 460 l 1,5,6
+ 533.536 452.388 533.536 452.388 539.674 445.246 c 0,7,8
+ 591.818 384.59 591.818 384.59 621.222 333.404 c 0,9,10
+ 649.427 284.306 649.427 284.306 665.429 249.104 c 0,11,12
+ 667.284 245.025 667.284 245.025 671.437 236.4 c 128,-1,13
+ 675.589 227.776 675.589 227.776 677.162 223.965 c 128,-1,14
+ 678.735 220.155 678.735 220.155 681.046 213.392 c 128,-1,15
+ 683.357 206.629 683.357 206.629 684.178 200.206 c 128,-1,16
+ 685 193.783 685 193.783 685 186 c 0,17,18
+ 685 168.111 685 168.111 676.078 150.264 c 128,-1,19
+ 667.155 132.417 667.155 132.417 650.239 122.268 c 0,20,21
+ 628.126 109 628.126 109 601 109 c 0,22,23
+ 562.875 109 562.875 109 541.438 130.438 c 0,24,25
+ 528.24 143.635 528.24 143.635 516.561 169.916 c 0,26,27
+ 469.006 272.477 469.006 272.477 399.263 349.194 c 0,28,29
+ 337.335 417.314 337.335 417.314 211.192 480.384 c 0,30,31
+ 202.353 484.803 202.353 484.803 195.21 489.565 c 128,-1,32
+ 188.149 494.273 188.149 494.273 182.31 499.278 c 0,33,34
+ 170.991 508.98 170.991 508.98 164.384 522.192 c 0,35,36
+ 157 536.96 157 536.96 157 555 c 0,37,38
+ 157 565.221 157 565.221 158.194 572.384 c 0,39,40
+ 159.313 579.101 159.313 579.101 161.486 584.891 c 128,-1,41
+ 163.659 590.682 163.659 590.682 165.713 594.27 c 128,-1,42
+ 167.767 597.858 167.767 597.858 171.056 601.384 c 128,-1,43
+ 174.346 604.91 174.346 604.91 176.034 606.284 c 128,-1,44
+ 177.722 607.658 177.722 607.658 180.939 609.888 c 128,-1,45
+ 184.156 612.117 184.156 612.117 184.4 612.3 c 0,46,47
+ 191.536 617.651 191.536 617.651 194.21 619.435 c 0,48,49
+ 197.794 621.824 197.794 621.824 215 631 c 2,50,-1
+ 216.025 631.547 l 1,51,-1
+ 217.073 632.046 l 2,52,53
+ 275.547 659.891 275.547 659.891 324.524 696.392 c 0,54,55
+ 373.814 733.128 373.814 733.128 403.127 763.236 c 0,56,57
+ 432.003 794.039 432.003 794.039 457.262 832.829 c 0,58,59
+ 486.682 878.009 486.682 878.009 492.775 891.939 c 0,60,61
+ 512.518 937.077 512.518 937.077 519.384 950.808 c 0,62,63
+ 524.259 960.558 524.259 960.558 526.768 964.739 c 0,64,65
+ 531.023 971.832 531.023 971.832 535.597 976.772 c 128,-1,66
+ 540.171 981.711 540.171 981.711 542.525 983.359 c 128,-1,67
+ 544.879 985.007 544.879 985.007 549.608 987.293 c 128,-1,68
+ 554.336 989.579 554.336 989.579 554.997 989.95 c 0,69,70
+ 574.642 1001 574.642 1001 601 1001 c 0,71,72
+ 630.778 1001 630.778 1001 653.299 985.591 c 0,73,74
+ 685 963.9 685 963.9 685 924 c 0,75,76
+ 685 916.203 685 916.203 684.179 909.776 c 128,-1,77
+ 683.357 903.348 683.357 903.348 681.052 896.6 c 128,-1,78
+ 678.746 889.851 678.746 889.851 677.167 886.032 c 128,-1,79
+ 675.589 882.212 675.589 882.212 671.444 873.611 c 128,-1,80
+ 667.298 865.01 667.298 865.01 665.429 860.896 c 0,81,82
+ 649.428 825.698 649.428 825.698 621.222 776.596 c 0,83,84
+ 591.768 725.32 591.768 725.32 539.529 665.086 c 0,85,86
+ 533.058 657.623 533.058 657.623 526.091 650 c 1,87,-1
+ 2122.05 650 l 1,88,-1
+ 2136.97 649.968 l 1,89,-1
+ 2148.09 649.97 l 1,90,-1
+ 2171.98 650 l 1,91,-1
+ 4581.99 650.5 l 2,92,93
+ 4599.28 650.503 4599.28 650.503 4610.18 649.93 c 0,94,95
+ 4625.98 649.098 4625.98 649.098 4645 643.245 c 0,96,97
+ 4676.03 633.694 4676.03 633.694 4692.12 608.234 c 0,98,99
+ 4706 586.265 4706 586.265 4706 555.5 c 128,-1,100
+ 4706 524.735 4706 524.735 4692.12 502.766 c 0,101,102
+ 4676.04 477.308 4676.04 477.308 4645 467.755 c 0,103,104
+ 4625.98 461.902 4625.98 461.902 4610.23 461.073 c 0,105,106
+ 4599.77 460.504 4599.77 460.504 4582.01 460.5 c 2,0,-1
+EndSplineSet
+EndChar
+
+StartChar: uni290F
+Encoding: 10511 10511 1390
+Width: 4862
+VWidth: 2220
+Flags: W
+HStem: 460 190<173.656 4330.97>
+LayerCount: 2
+Fore
+SplineSet
+4655.56 623.912 m 0,0,1
+ 4667.07 619.147 4667.07 619.147 4678.09 608.976 c 0,2,3
+ 4701 587.831 4701 587.831 4701 555.5 c 0,4,5
+ 4701 523.377 4701 523.377 4681.06 503.438 c 0,6,7
+ 4669.86 492.23 4669.86 492.23 4640.97 478.473 c 0,8,9
+ 4598.13 457.989 4598.13 457.989 4560.42 433.324 c 128,-1,10
+ 4522.52 408.528 4522.52 408.528 4495.91 386.042 c 0,11,12
+ 4470.1 364.224 4470.1 364.224 4446.25 336.361 c 0,13,14
+ 4421.13 306.958 4421.13 306.958 4406.25 286.503 c 0,15,16
+ 4392.15 267.13 4392.15 267.13 4377.19 239.922 c 0,17,18
+ 4361.46 211.319 4361.46 211.319 4357.28 202.576 c 1,19,20
+ 4351.19 184.828 4351.19 184.828 4338.62 159.692 c 0,21,22
+ 4332.2 146.864 4332.2 146.864 4326.82 140.141 c 0,23,24
+ 4319.4 130.857 4319.4 130.857 4304.03 121.252 c 2,25,-1
+ 4299.81 118.884 l 2,26,27
+ 4281.04 109.5 4281.04 109.5 4257 109.5 c 0,28,29
+ 4227.22 109.5 4227.22 109.5 4204.7 124.909 c 0,30,31
+ 4173 146.602 4173 146.602 4173 186.5 c 0,32,33
+ 4173 194.128 4173 194.128 4173.78 200.419 c 128,-1,34
+ 4174.55 206.71 4174.55 206.71 4176.78 213.429 c 128,-1,35
+ 4179 220.149 4179 220.149 4180.48 223.883 c 128,-1,36
+ 4181.97 227.617 4181.97 227.617 4186 236.294 c 128,-1,37
+ 4190.03 244.972 4190.03 244.972 4191.81 249.016 c 0,38,39
+ 4207.41 284.517 4207.41 284.517 4235.78 333.904 c 0,40,41
+ 4265.25 385.208 4265.25 385.208 4317.99 445.94 c 0,42,43
+ 4324.24 453.129 4324.24 453.129 4330.97 460.5 c 1,44,-1
+ 2734.04 460.5 l 1,45,-1
+ 2724.12 460.875 l 1,46,-1
+ 2716.39 460.875 l 1,47,-1
+ 2694.44 460.5 l 1,48,-1
+ 285.011 460 l 2,49,50
+ 267.683 459.996 267.683 459.996 257.171 460.579 c 0,51,52
+ 241.952 461.424 241.952 461.424 223.002 467.255 c 0,53,54
+ 192.97 476.496 192.97 476.496 176.409 500.701 c 0,55,56
+ 161 523.223 161 523.223 161 555 c 128,-1,57
+ 161 586.777 161 586.777 176.409 609.299 c 0,58,59
+ 192.971 633.505 192.971 633.505 223.002 642.745 c 0,60,61
+ 241.954 648.576 241.954 648.576 257.181 649.422 c 0,62,63
+ 267.571 649.997 267.571 649.997 284.989 650 c 2,64,-1
+ 2694.05 650.5 l 1,65,-1
+ 2714.07 650.457 l 1,66,-1
+ 2724.66 650.224 l 1,67,-1
+ 2734.27 650.5 l 1,68,-1
+ 4330.97 650.5 l 1,69,70
+ 4324.24 657.862 4324.24 657.862 4317.99 665.06 c 0,71,72
+ 4265.25 725.789 4265.25 725.789 4235.78 777.096 c 0,73,74
+ 4207.41 826.49 4207.41 826.49 4191.81 861.984 c 0,75,76
+ 4190.06 865.977 4190.06 865.977 4186.01 874.69 c 128,-1,77
+ 4181.96 883.404 4181.96 883.404 4180.49 887.123 c 128,-1,78
+ 4179.02 890.842 4179.02 890.842 4176.78 897.582 c 128,-1,79
+ 4174.55 904.322 4174.55 904.322 4173.78 910.607 c 128,-1,80
+ 4173 916.893 4173 916.893 4173 924.5 c 0,81,82
+ 4173 942.389 4173 942.389 4181.92 960.236 c 128,-1,83
+ 4190.85 978.083 4190.85 978.083 4207.76 988.232 c 0,84,85
+ 4229.87 1001.5 4229.87 1001.5 4257 1001.5 c 0,86,87
+ 4292.87 1001.5 4292.87 1001.5 4314.19 983.222 c 2,88,-1
+ 4317.17 980.669 l 1,89,-1
+ 4319.72 977.69 l 2,90,91
+ 4330.57 965.038 4330.57 965.038 4341.67 940.056 c 0,92,93
+ 4370.54 873.895 4370.54 873.895 4410.61 817.987 c 0,94,95
+ 4447.05 766.044 4447.05 766.044 4488.23 730.692 c 0,96,97
+ 4531.27 693.732 4531.27 693.732 4568.94 670.307 c 0,98,99
+ 4606.14 647.169 4606.14 647.169 4655.56 623.912 c 0,0,1
+EndSplineSet
+EndChar
 EndChars
 EndSplineFont

--- a/lib/texinputs/isabellesym.sty	Tue Dec 29 19:11:23 2015 +0100
+++ b/lib/texinputs/isabellesym.sty	Tue Dec 29 20:58:18 2015 +0100
@@ -158,8 +158,12 @@
 \newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
 \newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
 \newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
+\newcommand{\isasymlonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAA}}}}  %requires amsmath
+\newcommand{\isasymlonglonglongleftarrow}{\isamath{\xleftarrow{\hphantom{AAAA}}}}  %requires amsmath
 \newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
 \newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
+\newcommand{\isasymlonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAA}}}}  %requires amsmath
+\newcommand{\isasymlonglonglongrightarrow}{\isamath{\xrightarrow{\hphantom{AAAA}}}}  %requires amsmath
 \newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
 \newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
 \newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}

--- a/src/Doc/Isar_Ref/document/root.tex	Tue Dec 29 19:11:23 2015 +0100
+++ b/src/Doc/Isar_Ref/document/root.tex	Tue Dec 29 20:58:18 2015 +0100
@@ -1,6 +1,7 @@
 \documentclass[12pt,a4paper,fleqn]{report}
 \usepackage{lmodern}
 \usepackage[T1]{fontenc}
+\usepackage{amsmath}
 \usepackage{amssymb}
 \usepackage{wasysym}
 \usepackage{eurosym}