Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Merged
authorManuel Eberl <eberlm@in.tum.de>
Fri, 02 Sep 2016 08:54:46 +0200
changeset 63767 c2cbbd619f38
parent 63766 695d60817cb1 (current diff)
parent 63765 e60020520b15 (diff)
child 63768 a09cfea0c2c9
child 63770 a67397b13eb5
child 63772 4ad836f0b146
Merged
src/HOL/Word/Type_Length.thy file | annotate | diff | comparison | revisions 
--- a/Admin/components/components.sha1	Thu Sep 01 11:53:07 2016 +0200
+++ b/Admin/components/components.sha1	Fri Sep 02 08:54:46 2016 +0200
@@ -48,6 +48,7 @@
 878536aab1eaf1a52da560c20bb41ab942971fa3  isabelle_fonts-20160227.tar.gz
 8ff0eedf0191d808ecc58c6b3149a4697f29ab21  isabelle_fonts-20160812-1.tar.gz
 9283e3b0b4c7239f57b18e076ec8bb21021832cb  isabelle_fonts-20160812.tar.gz
+620cffeb125e198b91a716da116f754d6cc8174b  isabelle_fonts-20160830.tar.gz
 8d83e433c1419e0c0cc5fd1762903d11b4a5752c  jdk-6u31.tar.gz
 38d2d2a91c66714c18430e136e7e5191af3996e6  jdk-7u11.tar.gz
 d765bc4ad2f34d494429b2a8c1563c49db224944  jdk-7u13.tar.gz
--- a/Admin/components/main	Thu Sep 01 11:53:07 2016 +0200
+++ b/Admin/components/main	Fri Sep 02 08:54:46 2016 +0200
@@ -4,7 +4,7 @@
 cvc4-1.5pre-3
 e-1.8
 Haskabelle-2015
-isabelle_fonts-20160812-1
+isabelle_fonts-20160830
 jdk-8u102
 jedit_build-20160330
 jfreechart-1.0.14-1
--- a/NEWS	Thu Sep 01 11:53:07 2016 +0200
+++ b/NEWS	Fri Sep 02 08:54:46 2016 +0200
@@ -120,6 +120,13 @@
 occurences of the formal entity at the caret position. This facilitates
 systematic renaming.
 
+* Action "isabelle.keymap-merge" asks the user to resolve pending
+Isabelle keymap changes that are in conflict with the current jEdit
+keymap; non-conflicting changes are always applied implicitly. This
+action is automatically invoked on Isabelle/jEdit startup and thus
+increases chances that users see new keyboard shortcuts when re-using
+old keymaps.
+
 * Document markup works across multiple Isar commands, e.g. the results
 established at the end of a proof are properly identified in the theorem
 statement.
--- a/etc/symbols	Thu Sep 01 11:53:07 2016 +0200
+++ b/etc/symbols	Fri Sep 02 08:54:46 2016 +0200
@@ -385,3 +385,4 @@
 \<^dir>                 code: 0x01F5C0  group: icon  font: IsabelleText
 \<^url>                 code: 0x01F310  group: icon  font: IsabelleText
 \<^doc>                 code: 0x01F4D3  group: icon  font: IsabelleText
+\<^action>              code: 0x00261b  group: icon  font: IsabelleText
--- a/lib/fonts/IsabelleText.sfd	Thu Sep 01 11:53:07 2016 +0200
+++ b/lib/fonts/IsabelleText.sfd	Fri Sep 02 08:54:46 2016 +0200
@@ -19,7 +19,7 @@
 OS2_WeightWidthSlopeOnly: 0
 OS2_UseTypoMetrics: 1
 CreationTime: 1050361371
-ModificationTime: 1471012141
+ModificationTime: 1472550975
 PfmFamily: 17
 TTFWeight: 400
 TTFWidth: 5
@@ -2241,11 +2241,11 @@
 DisplaySize: -96
 AntiAlias: 1
 FitToEm: 1
-WinInfo: 128340 18 16
+WinInfo: 9684 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 1408
+BeginChars: 1114189 1409
 
 StartChar: u10000
 Encoding: 65536 65536 0
@@ -62747,5 +62747,53 @@
  841 238.4 l 1,54,-1
 EndSplineSet
 EndChar
+
+StartChar: uni261B
+Encoding: 9755 9755 1408
+Width: 1233
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+105 270 m 1,0,-1
+ 48 1046 l 1,1,2
+ 48 1088 48 1088 71.5 1117 c 128,-1,3
+ 95 1146 95 1146 127 1146 c 2,4,-1
+ 412 1146 l 2,5,6
+ 445 1146 445 1146 468 1117 c 0,7,8
+ 481 1101 481 1101 487 1080 c 1,9,-1
+ 1105 1080 l 2,10,11
+ 1125 1080 1125 1080 1144 1068 c 128,-1,12
+ 1163 1056 1163 1056 1174 1032 c 128,-1,13
+ 1185 1008 1185 1008 1185 982 c 0,14,15
+ 1185 941 1185 941 1161.5 912.5 c 128,-1,16
+ 1138 884 1138 884 1105 884 c 2,17,-1
+ 522 884 l 1,18,-1
+ 524 875 l 1,19,-1
+ 781 875 l 1,20,21
+ 798 873 798 873 813 862 c 0,22,23
+ 832 849 832 849 843.5 825.5 c 128,-1,24
+ 855 802 855 802 855 778 c 0,25,26
+ 855 737 855 737 831 708.5 c 128,-1,27
+ 807 680 807 680 756 680 c 2,28,-1
+ 560 680 l 1,29,-1
+ 561 670 l 1,30,-1
+ 698 670 l 2,31,32
+ 717 670 717 670 736.5 657 c 128,-1,33
+ 756 644 756 644 767 620.5 c 128,-1,34
+ 778 597 778 597 778 572 c 0,35,36
+ 778 531 778 531 754 502 c 0,37,38
+ 735 478 735 478 699 476 c 1,39,-1
+ 596 476 l 1,40,-1
+ 599 465 l 1,41,-1
+ 640 465 l 1,42,43
+ 654 462 654 462 668 453 c 0,44,45
+ 687 441 687 441 697.5 417.5 c 128,-1,46
+ 708 394 708 394 708 368 c 0,47,48
+ 708 328 708 328 685 299 c 128,-1,49
+ 662 270 662 270 629 270 c 2,50,-1
+ 105 270 l 1,0,-1
+EndSplineSet
+EndChar
 EndChars
 EndSplineFont
--- a/lib/fonts/IsabelleTextBold.sfd	Thu Sep 01 11:53:07 2016 +0200
+++ b/lib/fonts/IsabelleTextBold.sfd	Fri Sep 02 08:54:46 2016 +0200
@@ -20,7 +20,7 @@
 OS2_WeightWidthSlopeOnly: 0
 OS2_UseTypoMetrics: 1
 CreationTime: 1050374980
-ModificationTime: 1471012188
+ModificationTime: 1472550922
 PfmFamily: 17
 TTFWeight: 700
 TTFWidth: 5
@@ -1678,10 +1678,10 @@
 DisplaySize: -96
 AntiAlias: 1
 FitToEm: 1
-WinInfo: 127638 21 15
+WinInfo: 9513 21 15
 BeginPrivate: 0
 EndPrivate
-BeginChars: 1114115 1400
+BeginChars: 1114115 1401
 
 StartChar: .notdef
 Encoding: 1114112 -1 0
@@ -68861,87 +68861,87 @@
 LayerCount: 2
 Fore
 SplineSet
-1611.8 762 m 0
- 1611.8 444.06 1611.8 444.06 1386.86 219.138 c 0
- 1161.91 -5.7998 1161.91 -5.7998 844 -5.7998 c 0
- 526.07 -5.7998 526.07 -5.7998 301.138 219.138 c 0
- 76.2 444.08 76.2 444.08 76.2 762 c 0
- 76.2 1079.91 76.2 1079.91 301.138 1304.86 c 0
- 526.056 1529.8 526.056 1529.8 844 1529.8 c 0
- 1161.93 1529.8 1161.93 1529.8 1386.86 1304.86 c 0
- 1611.8 1079.93 1611.8 1079.93 1611.8 762 c 0
-1220.07 1261.11 m 1
- 1168.47 1300.23 1168.47 1300.23 1111.45 1327.2 c 1
- 1138.31 1275.55 1138.31 1275.55 1161.39 1221.76 c 1
- 1191.78 1240.21 1191.78 1240.21 1220.07 1261.11 c 1
-1465.7 833.3 m 1
- 1446.04 1018.25 1446.04 1018.25 1325.54 1161.18 c 1
- 1272.9 1119.91 1272.9 1119.91 1212.62 1085.87 c 1
- 1254.19 954.411 1254.19 954.411 1263.99 833.3 c 1
- 1465.7 833.3 l 1
-1032.07 1159.49 m 1
- 982.764 1277 982.764 1277 915.3 1379.54 c 1
- 915.3 1128.35 l 1
- 972.667 1137.3 972.667 1137.3 1032.07 1159.49 c 1
-772 1128.4 m 1
- 772 1378.3 l 1
- 705.395 1276.11 705.395 1276.11 656.076 1159.43 c 1
- 715.641 1137.24 715.641 1137.24 772 1128.4 c 1
-1120.11 833.3 m 1
- 1111.28 924.649 1111.28 924.649 1081.23 1024.49 c 1
- 996.9 993.412 996.9 993.412 915.3 983.737 c 1
- 915.3 833.3 l 1
- 1120.11 833.3 l 1
-1465.7 690 m 1
- 1263.98 690 l 1
- 1254.16 569.491 1254.16 569.491 1212.56 437.946 c 1
- 1272.5 403.924 1272.5 403.924 1325.48 362.623 c 1
- 1446.03 505.147 1446.03 505.147 1465.7 690 c 1
-576.794 1327.31 m 1
- 519.517 1300.22 519.517 1300.22 467.933 1261.11 c 1
- 496.214 1240.21 496.214 1240.21 526.679 1221.72 c 1
- 549.892 1275.64 549.892 1275.64 576.794 1327.31 c 1
-772 833.3 m 1
- 772 983.765 l 1
- 690.418 993.615 690.418 993.615 606.766 1024.48 c 1
- 576.71 924.621 576.71 924.621 567.891 833.3 c 1
- 772 833.3 l 1
-1120.09 690 m 1
- 915.3 690 l 1
- 915.3 540.263 l 1
- 996.899 530.588 996.899 530.588 1081.24 499.506 c 1
- 1111.27 599.254 1111.27 599.254 1120.09 690 c 1
-1220.07 262.892 m 1
- 1191.78 283.795 1191.78 283.795 1161.32 302.281 c 1
- 1138.12 248.387 1138.12 248.387 1111.21 196.689 c 1
- 1168.47 223.77 1168.47 223.77 1220.07 262.892 c 1
-475.438 1086.05 m 1
- 415.516 1120.07 415.516 1120.07 362.518 1161.37 c 1
- 241.972 1018.79 241.972 1018.79 222.285 833.3 c 1
- 424.006 833.3 l 1
- 433.81 954.411 433.81 954.411 475.438 1086.05 c 1
-772 540.235 m 1
- 772 690 l 1
- 567.914 690 l 1
- 576.734 599.257 576.734 599.257 606.761 499.515 c 1
- 690.429 530.386 690.429 530.386 772 540.235 c 1
-1031.92 364.563 m 1
- 972.259 386.759 972.259 386.759 915.3 395.651 c 1
- 915.3 144.624 l 1
- 982.429 247.46 982.429 247.46 1031.92 364.563 c 1
-772 145.521 m 1
- 772 395.601 l 1
- 715.225 386.699 715.225 386.699 655.924 364.514 c 1
- 704.843 247.924 704.843 247.924 772 145.521 c 1
-475.435 437.946 m 1
- 433.833 569.489 433.833 569.489 424.022 690 c 1
- 222.315 690 l 1
- 241.994 505.692 241.994 505.692 362.578 362.672 c 1
- 415.516 403.933 415.516 403.933 475.435 437.946 c 1
-576.794 196.689 m 1
- 549.878 248.388 549.878 248.388 526.679 302.281 c 1
- 496.212 283.788 496.212 283.788 467.933 262.892 c 1
- 519.514 223.78 519.514 223.78 576.794 196.689 c 1
+1611.8 762 m 0,0,1
+ 1611.8 444.06 1611.8 444.06 1386.86 219.138 c 0,2,3
+ 1161.91 -5.7998 1161.91 -5.7998 844 -5.7998 c 0,4,5
+ 526.07 -5.7998 526.07 -5.7998 301.138 219.138 c 0,6,7
+ 76.2 444.08 76.2 444.08 76.2 762 c 0,8,9
+ 76.2 1079.91 76.2 1079.91 301.138 1304.86 c 0,10,11
+ 526.056 1529.8 526.056 1529.8 844 1529.8 c 0,12,13
+ 1161.93 1529.8 1161.93 1529.8 1386.86 1304.86 c 0,14,15
+ 1611.8 1079.93 1611.8 1079.93 1611.8 762 c 0,0,1
+1220.07 1261.11 m 1,16,17
+ 1168.47 1300.23 1168.47 1300.23 1111.45 1327.2 c 1,18,19
+ 1138.31 1275.55 1138.31 1275.55 1161.39 1221.76 c 1,20,21
+ 1191.78 1240.21 1191.78 1240.21 1220.07 1261.11 c 1,16,17
+1465.7 833.3 m 1,22,23
+ 1446.04 1018.25 1446.04 1018.25 1325.54 1161.18 c 1,24,25
+ 1272.9 1119.91 1272.9 1119.91 1212.62 1085.87 c 1,26,27
+ 1254.19 954.411 1254.19 954.411 1263.99 833.3 c 1,28,-1
+ 1465.7 833.3 l 1,22,23
+1032.07 1159.49 m 1,29,30
+ 982.764 1277 982.764 1277 915.3 1379.54 c 1,31,-1
+ 915.3 1128.35 l 1,32,33
+ 972.667 1137.3 972.667 1137.3 1032.07 1159.49 c 1,29,30
+772 1128.4 m 1,34,-1
+ 772 1378.3 l 1,35,36
+ 705.395 1276.11 705.395 1276.11 656.076 1159.43 c 1,37,38
+ 715.641 1137.24 715.641 1137.24 772 1128.4 c 1,34,-1
+1120.11 833.3 m 1,39,40
+ 1111.28 924.649 1111.28 924.649 1081.23 1024.49 c 1,41,42
+ 996.9 993.412 996.9 993.412 915.3 983.737 c 1,43,-1
+ 915.3 833.3 l 1,44,-1
+ 1120.11 833.3 l 1,39,40
+1465.7 690 m 1,45,-1
+ 1263.98 690 l 1,46,47
+ 1254.16 569.491 1254.16 569.491 1212.56 437.946 c 1,48,49
+ 1272.5 403.924 1272.5 403.924 1325.48 362.623 c 1,50,51
+ 1446.03 505.147 1446.03 505.147 1465.7 690 c 1,45,-1
+576.794 1327.31 m 1,52,53
+ 519.517 1300.22 519.517 1300.22 467.933 1261.11 c 1,54,55
+ 496.214 1240.21 496.214 1240.21 526.679 1221.72 c 1,56,57
+ 549.892 1275.64 549.892 1275.64 576.794 1327.31 c 1,52,53
+772 833.3 m 1,58,-1
+ 772 983.765 l 1,59,60
+ 690.418 993.615 690.418 993.615 606.766 1024.48 c 1,61,62
+ 576.71 924.621 576.71 924.621 567.891 833.3 c 1,63,-1
+ 772 833.3 l 1,58,-1
+1120.09 690 m 1,64,-1
+ 915.3 690 l 1,65,-1
+ 915.3 540.263 l 1,66,67
+ 996.899 530.588 996.899 530.588 1081.24 499.506 c 1,68,69
+ 1111.27 599.254 1111.27 599.254 1120.09 690 c 1,64,-1
+1220.07 262.892 m 1,70,71
+ 1191.78 283.795 1191.78 283.795 1161.32 302.281 c 1,72,73
+ 1138.12 248.387 1138.12 248.387 1111.21 196.689 c 1,74,75
+ 1168.47 223.77 1168.47 223.77 1220.07 262.892 c 1,70,71
+475.438 1086.05 m 1,76,77
+ 415.516 1120.07 415.516 1120.07 362.518 1161.37 c 1,78,79
+ 241.972 1018.79 241.972 1018.79 222.285 833.3 c 1,80,-1
+ 424.006 833.3 l 1,81,82
+ 433.81 954.411 433.81 954.411 475.438 1086.05 c 1,76,77
+772 540.235 m 1,83,-1
+ 772 690 l 1,84,-1
+ 567.914 690 l 1,85,86
+ 576.734 599.257 576.734 599.257 606.761 499.515 c 1,87,88
+ 690.429 530.386 690.429 530.386 772 540.235 c 1,83,-1
+1031.92 364.563 m 1,89,90
+ 972.259 386.759 972.259 386.759 915.3 395.651 c 1,91,-1
+ 915.3 144.624 l 1,92,93
+ 982.429 247.46 982.429 247.46 1031.92 364.563 c 1,89,90
+772 145.521 m 1,94,-1
+ 772 395.601 l 1,95,96
+ 715.225 386.699 715.225 386.699 655.924 364.514 c 1,97,98
+ 704.843 247.924 704.843 247.924 772 145.521 c 1,94,-1
+475.435 437.946 m 1,99,100
+ 433.833 569.489 433.833 569.489 424.022 690 c 1,101,-1
+ 222.315 690 l 1,102,103
+ 241.994 505.692 241.994 505.692 362.578 362.672 c 1,104,105
+ 415.516 403.933 415.516 403.933 475.435 437.946 c 1,99,100
+576.794 196.689 m 1,106,107
+ 549.878 248.388 549.878 248.388 526.679 302.281 c 1,108,109
+ 496.212 283.788 496.212 283.788 467.933 262.892 c 1,110,111
+ 519.514 223.78 519.514 223.78 576.794 196.689 c 1,106,107
 EndSplineSet
 EndChar
 
@@ -68953,61 +68953,61 @@
 LayerCount: 2
 Fore
 SplineSet
-987.6 131.45 m 2
- 987.6 117.46 987.6 117.46 982.253 104.974 c 0
- 976.906 92.4875 976.906 92.4875 973.075 87.9227 c 0
- 969.244 83.3579 969.244 83.3579 960.649 74.2987 c 0
- 951.974 65.1552 951.974 65.1552 947.42 60.9378 c 0
- 942.865 56.7205 942.865 56.7205 929.937 50.7352 c 0
- 917.009 44.75 917.009 44.75 902.3 44.75 c 2
- 154.7 44.75 l 2
- 144.755 44.75 144.755 44.75 136.732 46.5759 c 0
- 128.708 48.4017 128.708 48.4017 123.042 52.0322 c 0
- 117.376 55.6626 117.376 55.6626 114.185 58.3353 c 0
- 110.995 61.0081 110.995 61.0081 107.166 65.5483 c 0
- 103.337 70.0886 103.337 70.0886 102.538 70.8876 c 0
- 101.738 71.6866 101.738 71.6866 97.1983 75.5157 c 0
- 92.6582 79.3449 92.6582 79.3449 89.9854 82.5355 c 0
- 87.3125 85.726 87.3125 85.726 83.6821 91.3921 c 0
- 80.0518 97.0581 80.0518 97.0581 78.2259 105.082 c 0
- 76.4 113.105 76.4 113.105 76.4 123.05 c 2
- 76.4 1202.45 l 2
- 76.4 1246.98 76.4 1246.98 114.258 1277.83 c 0
- 124.181 1285.77 124.181 1285.77 140.128 1292.56 c 0
- 156.075 1299.35 156.075 1299.35 185.287 1307.52 c 0
- 214.5 1315.68 214.5 1315.68 243.971 1322.98 c 0
- 273.442 1330.28 273.442 1330.28 329.44 1344.31 c 0
- 385.437 1358.34 385.437 1358.34 435.927 1371.78 c 0
- 469.093 1380.61 469.093 1380.61 514.719 1392.86 c 0
- 560.345 1405.11 560.345 1405.11 583.654 1411.34 c 0
- 606.963 1417.58 606.963 1417.58 637.85 1425.69 c 0
- 668.737 1433.8 668.737 1433.8 684.766 1437.64 c 0
- 700.795 1441.48 700.795 1441.48 718.697 1445.43 c 0
- 736.599 1449.39 736.599 1449.39 747.103 1450.82 c 0
- 757.606 1452.25 757.606 1452.25 765.1 1452.25 c 0
- 777.132 1452.25 777.132 1452.25 787.664 1450.49 c 0
- 816.159 1445.72 816.159 1445.72 837.129 1423.36 c 0
- 858.1 1400.99 858.1 1400.99 858.1 1370.45 c 2
- 858.1 1285.65 l 1
- 919.1 1285.65 l 2
- 952.854 1285.65 952.854 1285.65 973.808 1252.37 c 0
- 987.6 1230.47 987.6 1230.47 987.6 1210.15 c 2
- 987.6 131.45 l 2
-821.9 210.45 m 1
- 821.9 1122.05 l 1
- 284.8 1122.05 l 1
- 284.8 210.45 l 1
- 821.9 210.45 l 1
-811.2 725.15 m 1
- 302.5 725.15 l 1
- 302.5 1108.55 l 1
- 811.2 1108.55 l 1
- 811.2 725.15 l 1
-678.4 855.15 m 1
- 678.4 978.55 l 1
- 435.3 978.55 l 1
- 435.3 855.15 l 1
- 678.4 855.15 l 1
+987.6 131.45 m 2,0,1
+ 987.6 117.46 987.6 117.46 982.253 104.974 c 0,2,3
+ 976.906 92.4875 976.906 92.4875 973.075 87.9227 c 0,4,5
+ 969.244 83.3579 969.244 83.3579 960.649 74.2987 c 0,6,7
+ 951.974 65.1552 951.974 65.1552 947.42 60.9378 c 0,8,9
+ 942.865 56.7205 942.865 56.7205 929.937 50.7352 c 0,10,11
+ 917.009 44.75 917.009 44.75 902.3 44.75 c 2,12,-1
+ 154.7 44.75 l 2,13,14
+ 144.755 44.75 144.755 44.75 136.732 46.5759 c 0,15,16
+ 128.708 48.4017 128.708 48.4017 123.042 52.0322 c 0,17,18
+ 117.376 55.6626 117.376 55.6626 114.185 58.3353 c 0,19,20
+ 110.995 61.0081 110.995 61.0081 107.166 65.5483 c 0,21,22
+ 103.337 70.0886 103.337 70.0886 102.538 70.8876 c 0,23,24
+ 101.738 71.6866 101.738 71.6866 97.1983 75.5157 c 0,25,26
+ 92.6582 79.3449 92.6582 79.3449 89.9854 82.5355 c 0,27,28
+ 87.3125 85.726 87.3125 85.726 83.6821 91.3921 c 0,29,30
+ 80.0518 97.0581 80.0518 97.0581 78.2259 105.082 c 0,31,32
+ 76.4 113.105 76.4 113.105 76.4 123.05 c 2,33,-1
+ 76.4 1202.45 l 2,34,35
+ 76.4 1246.98 76.4 1246.98 114.258 1277.83 c 0,36,37
+ 124.181 1285.77 124.181 1285.77 140.128 1292.56 c 0,38,39
+ 156.075 1299.35 156.075 1299.35 185.287 1307.52 c 0,40,41
+ 214.5 1315.68 214.5 1315.68 243.971 1322.98 c 0,42,43
+ 273.442 1330.28 273.442 1330.28 329.44 1344.31 c 0,44,45
+ 385.437 1358.34 385.437 1358.34 435.927 1371.78 c 0,46,47
+ 469.093 1380.61 469.093 1380.61 514.719 1392.86 c 0,48,49
+ 560.345 1405.11 560.345 1405.11 583.654 1411.34 c 0,50,51
+ 606.963 1417.58 606.963 1417.58 637.85 1425.69 c 0,52,53
+ 668.737 1433.8 668.737 1433.8 684.766 1437.64 c 0,54,55
+ 700.795 1441.48 700.795 1441.48 718.697 1445.43 c 0,56,57
+ 736.599 1449.39 736.599 1449.39 747.103 1450.82 c 0,58,59
+ 757.606 1452.25 757.606 1452.25 765.1 1452.25 c 0,60,61
+ 777.132 1452.25 777.132 1452.25 787.664 1450.49 c 0,62,63
+ 816.159 1445.72 816.159 1445.72 837.129 1423.36 c 0,64,65
+ 858.1 1400.99 858.1 1400.99 858.1 1370.45 c 2,66,-1
+ 858.1 1285.65 l 1,67,-1
+ 919.1 1285.65 l 2,68,69
+ 952.854 1285.65 952.854 1285.65 973.808 1252.37 c 0,70,71
+ 987.6 1230.47 987.6 1230.47 987.6 1210.15 c 2,72,-1
+ 987.6 131.45 l 2,0,1
+821.9 210.45 m 1,73,-1
+ 821.9 1122.05 l 1,74,-1
+ 284.8 1122.05 l 1,75,-1
+ 284.8 210.45 l 1,76,-1
+ 821.9 210.45 l 1,73,-1
+811.2 725.15 m 1,77,-1
+ 302.5 725.15 l 1,78,-1
+ 302.5 1108.55 l 1,79,-1
+ 811.2 1108.55 l 1,80,-1
+ 811.2 725.15 l 1,77,-1
+678.4 855.15 m 1,81,-1
+ 678.4 978.55 l 1,82,-1
+ 435.3 978.55 l 1,83,-1
+ 435.3 855.15 l 1,84,-1
+ 678.4 855.15 l 1,81,-1
 EndSplineSet
 EndChar
 
@@ -69019,51 +69019,51 @@
 LayerCount: 2
 Fore
 SplineSet
-1081.5 163.65 m 2
- 1081.5 122.722 1081.5 122.722 1041.85 96.8642 c 0
- 1031.79 90.5761 1031.79 90.5761 1022.36 87.2552 c 0
- 1012.94 83.9343 1012.94 83.9343 1006.68 83.0855 c 0
- 1000.42 82.2367 1000.42 82.2367 986.754 81.065 c 0
- 973.093 79.8932 973.093 79.8932 962.975 78.4862 c 0
- 906.629 70.65 906.629 70.65 890.5 70.65 c 0
- 874.073 70.65 874.073 70.65 856.304 77.2317 c 0
- 838.536 83.8135 838.536 83.8135 824.647 92.1127 c 0
- 810.758 100.412 810.758 100.412 779.459 120.135 c 0
- 748.161 139.858 748.161 139.858 723.008 154.42 c 0
- 580.768 235.396 580.768 235.396 299.885 396.806 c 0
- 258.685 421.253 258.685 421.253 178.198 468.715 c 1
- 153.461 481.015 153.461 481.015 114.61 506.915 c 2
- 110.906 509.385 l 1
- 107.686 512.459 l 2
- 98.597 521.135 98.597 521.135 92.1108 530.717 c 0
- 76.5 553.779 76.5 553.779 76.5 580.15 c 2
- 76.5 1324.95 l 2
- 76.5 1358.02 76.5 1358.02 101.608 1376.08 c 0
- 126.716 1394.15 126.716 1394.15 152.7 1394.15 c 0
- 160.188 1394.15 160.188 1394.15 165.884 1393.16 c 0
- 171.581 1392.17 171.581 1392.17 173.948 1391.19 c 0
- 176.315 1390.21 176.315 1390.21 179.646 1388.28 c 0
- 182.977 1386.34 182.977 1386.34 184.004 1385.86 c 1
- 184.3 1409.27 l 2
- 184.3 1439.75 184.3 1439.75 206.971 1459.85 c 0
- 229.641 1479.96 229.641 1479.96 256.265 1482.17 c 2
- 272.065 1483.49 l 1
- 691.737 1243.39 l 1
- 727.276 1272.51 727.276 1272.51 756.51 1292.71 c 2
- 782.8 1310.87 l 1
- 1081.5 1141.89 l 1
- 1081.5 163.65 l 2
-923.5 948.388 m 1
- 923.5 1050.52 l 1
- 794.39 1125.14 l 1
- 728.336 1074.48 l 2
- 723.943 1071.54 723.943 1071.54 720.835 1068.73 c 1
- 923.5 948.388 l 1
-815 283.379 m 1
- 815 828.882 l 1
- 235.2 1169.98 l 1
- 235.2 617.33 l 1
- 815 283.379 l 1
+1081.5 163.65 m 2,0,1
+ 1081.5 122.722 1081.5 122.722 1041.85 96.8642 c 0,2,3
+ 1031.79 90.5761 1031.79 90.5761 1022.36 87.2552 c 0,4,5
+ 1012.94 83.9343 1012.94 83.9343 1006.68 83.0855 c 0,6,7
+ 1000.42 82.2367 1000.42 82.2367 986.754 81.065 c 0,8,9
+ 973.093 79.8932 973.093 79.8932 962.975 78.4862 c 0,10,11
+ 906.629 70.65 906.629 70.65 890.5 70.65 c 0,12,13
+ 874.073 70.65 874.073 70.65 856.304 77.2317 c 0,14,15
+ 838.536 83.8135 838.536 83.8135 824.647 92.1127 c 0,16,17
+ 810.758 100.412 810.758 100.412 779.459 120.135 c 0,18,19
+ 748.161 139.858 748.161 139.858 723.008 154.42 c 0,20,21
+ 580.768 235.396 580.768 235.396 299.885 396.806 c 0,22,23
+ 258.685 421.253 258.685 421.253 178.198 468.715 c 1,24,25
+ 153.461 481.015 153.461 481.015 114.61 506.915 c 2,26,-1
+ 110.906 509.385 l 1,27,-1
+ 107.686 512.459 l 2,28,29
+ 98.597 521.135 98.597 521.135 92.1108 530.717 c 0,30,31
+ 76.5 553.779 76.5 553.779 76.5 580.15 c 2,32,-1
+ 76.5 1324.95 l 2,33,34
+ 76.5 1358.02 76.5 1358.02 101.608 1376.08 c 0,35,36
+ 126.716 1394.15 126.716 1394.15 152.7 1394.15 c 0,37,38
+ 160.188 1394.15 160.188 1394.15 165.884 1393.16 c 0,39,40
+ 171.581 1392.17 171.581 1392.17 173.948 1391.19 c 0,41,42
+ 176.315 1390.21 176.315 1390.21 179.646 1388.28 c 0,43,44
+ 182.977 1386.34 182.977 1386.34 184.004 1385.86 c 1,45,-1
+ 184.3 1409.27 l 2,46,47
+ 184.3 1439.75 184.3 1439.75 206.971 1459.85 c 0,48,49
+ 229.641 1479.96 229.641 1479.96 256.265 1482.17 c 2,50,-1
+ 272.065 1483.49 l 1,51,-1
+ 691.737 1243.39 l 1,52,53
+ 727.276 1272.51 727.276 1272.51 756.51 1292.71 c 2,54,-1
+ 782.8 1310.87 l 1,55,-1
+ 1081.5 1141.89 l 1,56,-1
+ 1081.5 163.65 l 2,0,1
+923.5 948.388 m 1,57,-1
+ 923.5 1050.52 l 1,58,-1
+ 794.39 1125.14 l 1,59,-1
+ 728.336 1074.48 l 2,60,61
+ 723.943 1071.54 723.943 1071.54 720.835 1068.73 c 1,62,-1
+ 923.5 948.388 l 1,57,-1
+815 283.379 m 1,63,-1
+ 815 828.882 l 1,64,-1
+ 235.2 1169.98 l 1,65,-1
+ 235.2 617.33 l 1,66,-1
+ 815 283.379 l 1,63,-1
 EndSplineSet
 EndChar
 
@@ -69075,46 +69075,94 @@
 LayerCount: 2
 Fore
 SplineSet
-1165.12 71.72 m 1
- 150.881 71.72 l 1
- 150.881 1462.28 l 1
- 1165.12 1462.28 l 1
- 1165.12 71.72 l 1
-1021.12 215.72 m 1
- 1021.12 1318.28 l 1
- 294.881 1318.28 l 1
- 294.881 215.72 l 1
- 1021.12 215.72 l 1
-999.641 1165.4 m 1
- 316.359 1165.4 l 1
- 316.359 1309.4 l 1
- 999.641 1309.4 l 1
- 999.641 1165.4 l 1
-999.641 977.24 m 1
- 316.359 977.24 l 1
- 316.359 1121.24 l 1
- 999.641 1121.24 l 1
- 999.641 977.24 l 1
-999.641 789.08 m 1
- 316.359 789.08 l 1
- 316.359 933.08 l 1
- 999.641 933.08 l 1
- 999.641 789.08 l 1
-999.641 600.92 m 1
- 316.359 600.92 l 1
- 316.359 744.92 l 1
- 999.641 744.92 l 1
- 999.641 600.92 l 1
-999.641 412.76 m 1
- 316.359 412.76 l 1
- 316.359 556.76 l 1
- 999.641 556.76 l 1
- 999.641 412.76 l 1
-999.641 224.6 m 1
- 316.359 224.6 l 1
- 316.359 368.6 l 1
- 999.641 368.6 l 1
- 999.641 224.6 l 1
+1165.12 71.72 m 1,0,-1
+ 150.881 71.72 l 1,1,-1
+ 150.881 1462.28 l 1,2,-1
+ 1165.12 1462.28 l 1,3,-1
+ 1165.12 71.72 l 1,0,-1
+1021.12 215.72 m 1,4,-1
+ 1021.12 1318.28 l 1,5,-1
+ 294.881 1318.28 l 1,6,-1
+ 294.881 215.72 l 1,7,-1
+ 1021.12 215.72 l 1,4,-1
+999.641 1165.4 m 1,8,-1
+ 316.359 1165.4 l 1,9,-1
+ 316.359 1309.4 l 1,10,-1
+ 999.641 1309.4 l 1,11,-1
+ 999.641 1165.4 l 1,8,-1
+999.641 977.24 m 1,12,-1
+ 316.359 977.24 l 1,13,-1
+ 316.359 1121.24 l 1,14,-1
+ 999.641 1121.24 l 1,15,-1
+ 999.641 977.24 l 1,12,-1
+999.641 789.08 m 1,16,-1
+ 316.359 789.08 l 1,17,-1
+ 316.359 933.08 l 1,18,-1
+ 999.641 933.08 l 1,19,-1
+ 999.641 789.08 l 1,16,-1
+999.641 600.92 m 1,20,-1
+ 316.359 600.92 l 1,21,-1
+ 316.359 744.92 l 1,22,-1
+ 999.641 744.92 l 1,23,-1
+ 999.641 600.92 l 1,20,-1
+999.641 412.76 m 1,24,-1
+ 316.359 412.76 l 1,25,-1
+ 316.359 556.76 l 1,26,-1
+ 999.641 556.76 l 1,27,-1
+ 999.641 412.76 l 1,24,-1
+999.641 224.6 m 1,28,-1
+ 316.359 224.6 l 1,29,-1
+ 316.359 368.6 l 1,30,-1
+ 999.641 368.6 l 1,31,-1
+ 999.641 224.6 l 1,28,-1
+EndSplineSet
+EndChar
+
+StartChar: uni261B
+Encoding: 9755 9755 1400
+Width: 1233
+Flags: W
+LayerCount: 2
+Fore
+SplineSet
+105 270 m 1,0,-1
+ 48 1046 l 1,1,2
+ 48 1087 48 1087 71.5 1116.5 c 128,-1,3
+ 95 1146 95 1146 127 1146 c 2,4,-1
+ 412 1146 l 2,5,6
+ 445 1146 445 1146 468 1117 c 0,7,8
+ 480 1101 480 1101 487 1080 c 1,9,-1
+ 1105 1080 l 2,10,11
+ 1125 1080 1125 1080 1144 1068 c 128,-1,12
+ 1163 1056 1163 1056 1174 1032 c 128,-1,13
+ 1185 1008 1185 1008 1185 982 c 0,14,15
+ 1185 941 1185 941 1161.5 912.5 c 128,-1,16
+ 1138 884 1138 884 1105 884 c 2,17,-1
+ 522 884 l 1,18,-1
+ 524 875 l 1,19,-1
+ 781 875 l 1,20,21
+ 798 872 798 872 813 862 c 0,22,23
+ 832 849 832 849 843.5 825.5 c 128,-1,24
+ 855 802 855 802 855 778 c 0,25,26
+ 855 737 855 737 831 708.5 c 128,-1,27
+ 807 680 807 680 756 680 c 2,28,-1
+ 560 680 l 1,29,-1
+ 561 670 l 1,30,-1
+ 698 670 l 2,31,32
+ 718 670 718 670 737 657 c 128,-1,33
+ 756 644 756 644 767 620.5 c 128,-1,34
+ 778 597 778 597 778 572 c 0,35,36
+ 778 530 778 530 754 502 c 1,37,38
+ 735 478 735 478 699 476 c 1,39,-1
+ 596 476 l 1,40,-1
+ 599 465 l 1,41,-1
+ 640 465 l 1,42,43
+ 654 462 654 462 668 453 c 0,44,45
+ 687 441 687 441 697.5 417.5 c 128,-1,46
+ 708 394 708 394 708 368 c 0,47,48
+ 708 328 708 328 685 299 c 128,-1,49
+ 662 270 662 270 629 270 c 2,50,-1
+ 105 270 l 1,0,-1
 EndSplineSet
 EndChar
 EndChars
--- a/src/Doc/JEdit/JEdit.thy	Thu Sep 01 11:53:07 2016 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Fri Sep 02 08:54:46 2016 +0200
@@ -166,8 +166,7 @@
   Regular jEdit options are accessible via the dialogs \<^emph>\<open>Utilities~/ Global
   Options\<close> or \<^emph>\<open>Plugins~/ Plugin Options\<close>, with a second chance to flip the
   two within the central options dialog. Changes are stored in @{path
-  "$ISABELLE_HOME_USER/jedit/properties"} and @{path
-  "$ISABELLE_HOME_USER/jedit/keymaps"}.
+  "$JEDIT_SETTINGS/properties"} and @{path "$JEDIT_SETTINGS/keymaps"}.
 
   Isabelle system options are managed by Isabelle/Scala and changes are stored
   in @{path "$ISABELLE_HOME_USER/etc/preferences"}, independently of
@@ -193,7 +192,7 @@
   \<^medskip>
   Options are usually loaded on startup and saved on shutdown of
   Isabelle/jEdit. Editing the machine-generated @{path
-  "$ISABELLE_HOME_USER/jedit/properties"} or @{path
+  "$JEDIT_SETTINGS/properties"} or @{path
   "$ISABELLE_HOME_USER/etc/preferences"} manually while the application is
   running is likely to cause surprise due to lost update!
 \<close>
@@ -212,8 +211,8 @@
   Isabelle/jEdit due to various fine-tuning of global defaults, with
   additional keyboard shortcuts for Isabelle-specific functionality. Users may
   change their keymap later, but need to copy some keyboard shortcuts manually
-  (see also @{path "$ISABELLE_HOME_USER/jedit/keymaps"} versus \<^verbatim>\<open>shortcut\<close>
-  properties in \<^file>\<open>$ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props\<close>).
+  (see also @{path "$JEDIT_SETTINGS/keymaps"} versus \<^verbatim>\<open>shortcut\<close> properties in
+  \<^file>\<open>$JEDIT_HOME/src/jEdit.props\<close>).
 \<close>
 
 
@@ -671,10 +670,11 @@
   wrapper, in contrast to @{tool jedit} run from the command line
   (\secref{sec:command-line}).
 
-  Isabelle/jEdit imitates \<^verbatim>\<open>$ISABELLE_HOME\<close> and \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> within
-  the Java process environment, in order to allow easy access to these
-  important places from the editor. The file browser of jEdit also includes
-  \<^emph>\<open>Favorites\<close> for these two important locations.
+  Isabelle/jEdit imitates important system settings within the Java process
+  environment, in order to allow easy access to these important places from
+  the editor: \<^verbatim>\<open>$ISABELLE_HOME\<close>, \<^verbatim>\<open>$ISABELLE_HOME_USER\<close>, \<^verbatim>\<open>$JEDIT_HOME\<close>,
+  \<^verbatim>\<open>$JEDIT_SETTINGS\<close>. The file browser of jEdit also includes \<^emph>\<open>Favorites\<close> for
+  these two important locations.
 
   \<^medskip>
   Path specifications in prover input or output usually include formal markup
--- a/src/HOL/Data_Structures/Balance_List.thy	Thu Sep 01 11:53:07 2016 +0200
+++ b/src/HOL/Data_Structures/Balance_List.thy	Fri Sep 02 08:54:46 2016 +0200
@@ -20,7 +20,8 @@
 definition "balance xs = fst (bal xs (length xs))"
 
 lemma bal_inorder:
-  "bal xs n = (t,ys) \<Longrightarrow> n \<le> length xs \<Longrightarrow> inorder t = take n xs \<and> ys = drop n xs"
+  "\<lbrakk> bal xs n = (t,ys); n \<le> length xs \<rbrakk>
+  \<Longrightarrow> inorder t = take n xs \<and> ys = drop n xs"
 proof(induction xs n arbitrary: t ys rule: bal.induct)
   case (1 xs n) show ?case
   proof cases
@@ -112,14 +113,14 @@
 qed
 
 lemma balanced_bal:
-  assumes "bal xs n = (t,ys)" shows "height t - min_height t \<le> 1"
+  assumes "bal xs n = (t,ys)" shows "balanced t"
 proof -
   have "floorlog 2 n \<le> floorlog 2 (n+1)" by (rule floorlog_mono) auto
   thus ?thesis
     using bal_height[OF assms] bal_min_height[OF assms] by arith
 qed
 
-corollary balanced_balance: "height(balance xs) - min_height(balance xs) \<le> 1"
+corollary balanced_balance: "balanced (balance xs)"
 by (metis balance_def balanced_bal prod.collapse)
 
 end
--- a/src/HOL/Library/Library.thy	Thu Sep 01 11:53:07 2016 +0200
+++ b/src/HOL/Library/Library.thy	Fri Sep 02 08:54:46 2016 +0200
@@ -83,6 +83,7 @@
   Sum_of_Squares
   Transitive_Closure_Table
   Tree_Multiset
+  Type_Length
   While_Combinator
 begin
 end
--- a/src/HOL/Library/Polynomial_Factorial.thy	Thu Sep 01 11:53:07 2016 +0200
+++ b/src/HOL/Library/Polynomial_Factorial.thy	Fri Sep 02 08:54:46 2016 +0200
@@ -1,3 +1,11 @@
+(*  Title:      HOL/Library/Polynomial_Factorial.thy
+    Author:     Brian Huffman
+    Author:     Clemens Ballarin
+    Author:     Amine Chaieb
+    Author:     Florian Haftmann
+    Author:     Manuel Eberl
+*)
+
 theory Polynomial_Factorial
 imports 
   Complex_Main
@@ -1470,4 +1478,4 @@
   
 value [code] "Lcm {[:1,2,3:], [:2,3,4::int poly:]}"
 
-end
\ No newline at end of file
+end
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Sep 01 11:53:07 2016 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Fri Sep 02 08:54:46 2016 +0200
@@ -1,5 +1,9 @@
+(*  Title:      HOL/Library/Predicate_Compile_Alternative_Defs.thy
+    Author:     Lukas Bulwahn, TU Muenchen
+*)
+
 theory Predicate_Compile_Alternative_Defs
-imports Main
+  imports Main
 begin
 
 section \<open>Common constants\<close>
--- a/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Thu Sep 01 11:53:07 2016 +0200
+++ b/src/HOL/Library/Predicate_Compile_Quickcheck.thy	Fri Sep 02 08:54:46 2016 +0200
@@ -1,9 +1,11 @@
-(* Author: Lukas Bulwahn, TU Muenchen *)
+(*  Title:      HOL/Library/Predicate_Compile_Alternative_Defs.thy
+    Author:     Lukas Bulwahn, TU Muenchen
+*)
 
 section \<open>A Prototype of Quickcheck based on the Predicate Compiler\<close>
 
 theory Predicate_Compile_Quickcheck
-imports Main Predicate_Compile_Alternative_Defs
+  imports Predicate_Compile_Alternative_Defs
 begin
 
 ML_file "../Tools/Predicate_Compile/predicate_compile_quickcheck.ML"
--- a/src/HOL/Library/Saturated.thy	Thu Sep 01 11:53:07 2016 +0200
+++ b/src/HOL/Library/Saturated.thy	Fri Sep 02 08:54:46 2016 +0200
@@ -7,7 +7,7 @@
 section \<open>Saturated arithmetic\<close>
 
 theory Saturated
-imports Numeral_Type "~~/src/HOL/Word/Type_Length"
+imports Numeral_Type Type_Length
 begin
 
 subsection \<open>The type of saturated naturals\<close>
--- a/src/HOL/Library/Tree.thy	Thu Sep 01 11:53:07 2016 +0200
+++ b/src/HOL/Library/Tree.thy	Fri Sep 02 08:54:46 2016 +0200
@@ -1,4 +1,8 @@
 (* Author: Tobias Nipkow *)
+(* Todo:
+ size t = 2^h - 1 \<Longrightarrow> complete t
+ (min_)height of balanced trees via floorlog
+*)
 
 section \<open>Binary Tree\<close>
 
@@ -85,6 +89,9 @@
   qed
 qed simp
 
+corollary size_height: "size t \<le> 2 ^ height (t::'a tree) - 1"
+using size1_height[of t] by(arith)
+
 
 fun min_height :: "'a tree \<Rightarrow> nat" where
 "min_height Leaf = 0" |
@@ -106,23 +113,114 @@
 qed simp
 
 
-subsection "Balanced"
+subsection \<open>Complete\<close>
 
-fun balanced :: "'a tree \<Rightarrow> bool" where
-"balanced Leaf = True" |
-"balanced (Node l x r) = (balanced l \<and> balanced r \<and> height l = height r)"
+fun complete :: "'a tree \<Rightarrow> bool" where
+"complete Leaf = True" |
+"complete (Node l x r) = (complete l \<and> complete r \<and> height l = height r)"
 
-lemma balanced_iff_min_height: "balanced t \<longleftrightarrow> (min_height t = height t)"
+lemma complete_iff_height: "complete t \<longleftrightarrow> (min_height t = height t)"
 apply(induction t)
  apply simp
 apply (simp add: min_def max_def)
 by (metis le_antisym le_trans min_hight_le_height)
 
-lemma balanced_size1: "balanced t \<Longrightarrow> size1 t = 2 ^ height t"
+lemma complete_size1: "complete t \<Longrightarrow> size1 t = 2 ^ height t"
 by (induction t) auto
 
-lemma balanced_size: "balanced t \<Longrightarrow> size t = 2 ^ height t - 1"
-using balanced_size1[simplified size1_def] by fastforce
+lemma size_if_complete: "complete t \<Longrightarrow> size t = 2 ^ height t - 1"
+using complete_size1[simplified size1_def] by fastforce
+
+text\<open>A better lower bound for incomplete trees:\<close>
+
+lemma min_height_le_size_if_incomplete:
+  "\<not> complete t \<Longrightarrow> 2 ^ min_height t \<le> size t"
+proof(induction t)
+  case Leaf thus ?case by simp
+next
+  case (Node l a r)
+  show ?case (is "?l \<le> ?r")
+  proof (cases "complete l")
+    case l: True thus ?thesis
+    proof (cases "complete r")
+      case r: True
+      have "height l \<noteq> height r" using Node.prems l r by simp
+      hence "?l < 2 ^ min_height l + 2 ^ min_height r"
+        using l r by (simp add: min_def complete_iff_height)
+      also have "\<dots> = (size l + 1) + (size r + 1)"
+        using l r size_if_complete[where ?'a = 'a]
+        by (simp add: complete_iff_height)
+      also have "\<dots> \<le> ?r + 1" by simp
+      finally show ?thesis by arith
+    next
+      case r: False
+      have "?l \<le> 2 ^ min_height l + 2 ^ min_height r" by (simp add: min_def)
+      also have "\<dots> \<le> size l + 1 + size r"
+        using Node.IH(2)[OF r] l size_if_complete[where ?'a = 'a]
+        by (simp add: complete_iff_height)
+      also have "\<dots> = ?r" by simp
+      finally show ?thesis .
+    qed
+  next
+    case l: False thus ?thesis
+    proof (cases "complete r")
+      case r: True
+      have "?l \<le> 2 ^ min_height l + 2 ^ min_height r" by (simp add: min_def)
+      also have "\<dots> \<le> size l + (size r + 1)"
+        using Node.IH(1)[OF l] r size_if_complete[where ?'a = 'a]
+        by (simp add: complete_iff_height)
+      also have "\<dots> = ?r" by simp
+      finally show ?thesis .
+    next
+      case r: False
+      have "?l \<le> 2 ^ min_height l + 2 ^ min_height r"
+        by (simp add: min_def)
+      also have "\<dots> \<le> size l + size r"
+        using Node.IH(1)[OF l] Node.IH(2)[OF r] by (simp)
+      also have "\<dots> \<le> ?r" by simp
+      finally show ?thesis .
+    qed
+  qed
+qed
+
+
+subsection \<open>Balanced\<close>
+
+abbreviation "balanced t \<equiv> (height t - min_height t \<le> 1)"
+
+text\<open>Balanced trees have optimal height:\<close>
+
+lemma balanced_optimal:
+fixes t :: "'a tree" and t' :: "'b tree"
+assumes "balanced t" "size t \<le> size t'" shows "height t \<le> height t'"
+proof (cases "complete t")
+  case True
+  have "(2::nat) ^ height t - 1 \<le> 2 ^ height t' - 1"
+  proof -
+    have "(2::nat) ^ height t - 1 = size t"
+      using True by (simp add: complete_iff_height size_if_complete)
+    also note assms(2)
+    also have "size t' \<le> 2 ^ height t' - 1" by (rule size_height)
+    finally show ?thesis .
+  qed
+  thus ?thesis by (simp add: le_diff_iff)
+next
+  case False
+  have "(2::nat) ^ min_height t < 2 ^ height t'"
+  proof -
+    have "(2::nat) ^ min_height t \<le> size t"
+      by(rule min_height_le_size_if_incomplete[OF False])
+    also note assms(2)
+    also have "size t' \<le> 2 ^ height t' - 1"  by(rule size_height)
+    finally show ?thesis
+      using power_eq_0_iff[of "2::nat" "height t'"] by linarith
+  qed
+  hence *: "min_height t < height t'" by simp
+  have "min_height t + 1 = height t"
+    using min_hight_le_height[of t] assms(1) False
+    by (simp add: complete_iff_height)
+  with * show ?thesis by arith
+qed
 
 
 subsection \<open>Path length\<close>
@@ -133,7 +231,7 @@
 "path_len Leaf = 0 " |
 "path_len (Node l _ r) = path_len l + size l + path_len r + size r"
 
-lemma path_len_if_bal: "balanced t
+lemma path_len_if_bal: "complete t
   \<Longrightarrow> path_len t = (let n = height t in 2 + n*2^n - 2^(n+1))"
 proof(induction t)
   case (Node l x r)
@@ -141,7 +239,7 @@
     by(induction n) auto
   have **: "(0::nat) < 2^n" for n :: nat by simp
   let ?h = "height r"
-  show ?case using Node *[of ?h] **[of ?h] by (simp add: balanced_size Let_def)
+  show ?case using Node *[of ?h] **[of ?h] by (simp add: size_if_complete Let_def)
 qed simp
 
 
@@ -171,6 +269,12 @@
 "inorder \<langle>\<rangle> = []" |
 "inorder \<langle>l, x, r\<rangle> = inorder l @ [x] @ inorder r"
 
+text\<open>A linear version avoiding append:\<close>
+fun inorder2 :: "'a tree \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"inorder2 \<langle>\<rangle> xs = xs" |
+"inorder2 \<langle>l, x, r\<rangle> xs = inorder2 l (x # inorder2 r xs)"
+
+
 lemma set_inorder[simp]: "set (inorder t) = set_tree t"
 by (induction t) auto
 
@@ -189,6 +293,9 @@
 lemma inorder_map: "inorder (map_tree f t) = map f (inorder t)"
 by (induction t) auto
 
+lemma inorder2_inorder: "inorder2 t xs = inorder t @ xs"
+by (induction t arbitrary: xs) auto
+
 
 subsection \<open>Binary Search Tree predicate\<close>
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Type_Length.thy	Fri Sep 02 08:54:46 2016 +0200
@@ -0,0 +1,54 @@
+(*  Title:      HOL/Library/Type_Length.thy
+    Author:     John Matthews, Galois Connections, Inc., Copyright 2006
+*)
+
+section \<open>Assigning lengths to types by type classes\<close>
+
+theory Type_Length
+imports Numeral_Type
+begin
+
+text \<open>
+  The aim of this is to allow any type as index type, but to provide a
+  default instantiation for numeral types. This independence requires
+  some duplication with the definitions in \<^file>\<open>Numeral_Type.thy\<close>.
+\<close>
+
+class len0 =
+  fixes len_of :: "'a itself \<Rightarrow> nat"
+
+text \<open>Some theorems are only true on words with length greater 0.\<close>
+
+class len = len0 +
+  assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)"
+
+instantiation num0 and num1 :: len0
+begin
+
+definition len_num0: "len_of (_ :: num0 itself) = 0"
+definition len_num1: "len_of (_ :: num1 itself) = 1"
+
+instance ..
+
+end
+
+instantiation bit0 and bit1 :: (len0) len0
+begin
+
+definition len_bit0: "len_of (_ :: 'a::len0 bit0 itself) = 2 * len_of TYPE('a)"
+definition len_bit1: "len_of (_ :: 'a::len0 bit1 itself) = 2 * len_of TYPE('a) + 1"
+
+instance ..
+
+end
+
+lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
+
+instance num1 :: len
+  by standard simp
+instance bit0 :: (len) len
+  by standard simp
+instance bit1 :: (len0) len
+  by standard simp
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Nesting.thy	Fri Sep 02 08:54:46 2016 +0200
@@ -0,0 +1,19 @@
+theory Quickcheck_Nesting
+imports Main
+begin
+
+ML \<open>
+let
+  open BNF_FP_Def_Sugar
+  open BNF_LFP_Compat
+
+  val compat_plugin = Plugin_Name.declare_setup @{binding compat};
+
+  fun compat fp_sugars =
+    perhaps (try (datatype_compat (map (fst o dest_Type o #T) fp_sugars)));
+in
+  Theory.setup (fp_sugars_interpretation compat_plugin compat)
+end
+\<close>
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Quickcheck_Examples/Quickcheck_Nesting_Example.thy	Fri Sep 02 08:54:46 2016 +0200
@@ -0,0 +1,11 @@
+theory Quickcheck_Nesting_Example
+imports Quickcheck_Nesting
+begin
+
+datatype x = X "x list"
+
+lemma "X a = X b"
+quickcheck[exhaustive, size = 4, expect = counterexample]
+oops
+
+end
--- a/src/HOL/ROOT	Thu Sep 01 11:53:07 2016 +0200
+++ b/src/HOL/ROOT	Fri Sep 02 08:54:46 2016 +0200
@@ -31,8 +31,12 @@
   *}
   theories
     Library
+    Nonpos_Ints
+    Periodic_Fun
+    Polynomial_Factorial
+    Predicate_Compile_Quickcheck
+    Prefix_Order
     Rewrite
-    Nonpos_Ints
     (*conflicting type class instantiations*)
     List_lexord
     Sublist_Order
@@ -978,6 +982,7 @@
     Quickcheck_Lattice_Examples
     Completeness
     Quickcheck_Interfaces
+    Quickcheck_Nesting_Example
   theories [condition = ISABELLE_GHC]
     Hotel_Example
     Quickcheck_Narrowing_Examples
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Thu Sep 01 11:53:07 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Fri Sep 02 08:54:46 2016 +0200
@@ -221,7 +221,7 @@
     val fpTs0 as Type (_, var_As) :: _ =
       map (#T o checked_fp_sugar_of o fst o dest_Type)
         (#Ts (#fp_res (checked_fp_sugar_of (hd fpT_names0))));
-    val fpT_names = map (fst o dest_Type) fpTs0;
+    val fpT_names as fpT_name1 :: _ = map (fst o dest_Type) fpTs0;
 
     val _ = check_names (op =) (fpT_names0, fpT_names) orelse not_mutually_recursive fpT_names0;
 
@@ -237,7 +237,8 @@
     fun mk_typ_descr index (Type (T_name, Ts)) ({ctrs, ...} : ctr_sugar) =
       (index, (T_name, map mk_dtyp Ts, map (mk_ctr_descr Ts) ctrs));
 
-    val fp_ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar o checked_fp_sugar_of) fpT_names;
+    val fp_sugars as {fp, ...} :: _ = map checked_fp_sugar_of fpT_names;
+    val fp_ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar) fp_sugars;
     val orig_descr = @{map 3} mk_typ_descr (0 upto nn_fp - 1) fpTs fp_ctr_sugars;
     val all_infos = Old_Datatype_Data.get_all thy;
     val (orig_descr' :: nested_descrs) =
@@ -310,11 +311,13 @@
       if member (op =) prefs Keep_Nesting orelse
          not (exists (exists (exists is_nested_rec_type)) ctrXs_Tsss') then
         ((lfp_sugar_thms', (inducts, induct, recs, rec_thmss)), lthy')
-      else
+      else if fp = Least_FP then
         define_split_rec_derive_induct_rec_thms Xs' fpTs' ctrXs_Tsss' ctrss' inducts induct recs
           rec_thmss lthy'
         |>> `(fn (inducts', induct', _, rec'_thmss) =>
-          SOME ((inducts', induct', mk_induct_attrs ctrss'), (rec'_thmss, [])));
+          SOME ((inducts', induct', mk_induct_attrs ctrss'), (rec'_thmss, [])))
+      else
+        not_datatype fpT_name1;
 
     val rec'_names = map (fst o dest_Const) recs';
     val rec'_thms = flat rec'_thmss;
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Sep 01 11:53:07 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Fri Sep 02 08:54:46 2016 +0200
@@ -49,7 +49,7 @@
 
 (* static options *)
 
-val compat_prefs = [BNF_LFP_Compat.Keep_Nesting, BNF_LFP_Compat.Include_GFPs]
+val compat_prefs = [BNF_LFP_Compat.Include_GFPs]
 
 val define_foundationally = false
 
--- a/src/HOL/Word/Type_Length.thy	Thu Sep 01 11:53:07 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(*  Title:      HOL/Word/Type_Length.thy
-    Author:     John Matthews, Galois Connections, Inc., copyright 2006
-*)
-
-section \<open>Assigning lengths to types by typeclasses\<close>
-
-theory Type_Length
-imports "~~/src/HOL/Library/Numeral_Type"
-begin
-
-text \<open>
-  The aim of this is to allow any type as index type, but to provide a
-  default instantiation for numeral types. This independence requires
-  some duplication with the definitions in \<open>Numeral_Type\<close>.
-\<close>
-
-class len0 =
-  fixes len_of :: "'a itself \<Rightarrow> nat"
-
-text \<open>
-  Some theorems are only true on words with length greater 0.
-\<close>
-
-class len = len0 +
-  assumes len_gt_0 [iff]: "0 < len_of TYPE ('a)"
-
-instantiation num0 and num1 :: len0
-begin
-
-definition
-  len_num0:  "len_of (x::num0 itself) = 0"
-
-definition
-  len_num1: "len_of (x::num1 itself) = 1"
-
-instance ..
-
-end
-
-instantiation bit0 and bit1 :: (len0) len0
-begin
-
-definition
-  len_bit0: "len_of (x::'a::len0 bit0 itself) = 2 * len_of TYPE ('a)"
-
-definition
-  len_bit1: "len_of (x::'a::len0 bit1 itself) = 2 * len_of TYPE ('a) + 1"
-
-instance ..
-
-end
-
-lemmas len_of_numeral_defs [simp] = len_num0 len_num1 len_bit0 len_bit1
-
-instance num1 :: len proof qed simp
-instance bit0 :: (len) len proof qed simp
-instance bit1 :: (len0) len proof qed simp
-
-end
-
--- a/src/HOL/Word/Word.thy	Thu Sep 01 11:53:07 2016 +0200
+++ b/src/HOL/Word/Word.thy	Fri Sep 02 08:54:46 2016 +0200
@@ -6,7 +6,7 @@
 
 theory Word
 imports
-  Type_Length
+  "~~/src/HOL/Library/Type_Length"
   "~~/src/HOL/Library/Boolean_Algebra"
   Bits_Bit
   Bool_List_Representation
--- a/src/Pure/General/completion.scala	Thu Sep 01 11:53:07 2016 +0200
+++ b/src/Pure/General/completion.scala	Fri Sep 02 08:54:46 2016 +0200
@@ -208,8 +208,10 @@
         } yield {
           val description = List(xname1, "(" + descr_name + ")")
           val replacement =
-            Token.explode(Keyword.Keywords.empty, xname1) match {
-              case List(tok) if tok.is_name => xname1
+            List(original, xname1).map(Token.explode(Keyword.Keywords.empty, _)) match {
+              case List(List(tok), _) if tok.kind == Token.Kind.CARTOUCHE =>
+                Symbol.open_decoded + xname1 + Symbol.close_decoded
+              case List(_, List(tok)) if tok.is_name => xname1
               case _ => quote(xname1)
             }
           Item(range, original, full_name, description, replacement, 0, true)
--- a/src/Pure/Tools/main.scala	Thu Sep 01 11:53:07 2016 +0200
+++ b/src/Pure/Tools/main.scala	Fri Sep 02 08:54:46 2016 +0200
@@ -100,11 +100,15 @@
     {
       val isabelle_home = Isabelle_System.getenv("ISABELLE_HOME")
       val isabelle_home_user = Isabelle_System.getenv("ISABELLE_HOME_USER")
+      val jedit_home = Isabelle_System.getenv("JEDIT_HOME")
+      val jedit_settings = Isabelle_System.getenv("JEDIT_SETTINGS")
 
       (env0: Any) => {
         val env = env0.asInstanceOf[java.util.Map[String, String]]
         env.put("ISABELLE_HOME", File.platform_path(isabelle_home))
         env.put("ISABELLE_HOME_USER", File.platform_path(isabelle_home_user))
+        env.put("JEDIT_HOME", File.platform_path(jedit_home))
+        env.put("JEDIT_SETTINGS", File.platform_path(jedit_settings))
         env.remove("ISABELLE_ROOT")
       }
     }
--- a/src/Pure/library.scala	Thu Sep 01 11:53:07 2016 +0200
+++ b/src/Pure/library.scala	Fri Sep 02 08:54:46 2016 +0200
@@ -187,4 +187,11 @@
   def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs
   def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs
   def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
+
+  def distinct[A](xs: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] =
+  {
+    val result = new mutable.ListBuffer[A]
+    for (x <- xs if !result.exists(y => eq(x, y))) result += x
+    result.toList
+  }
 }
--- a/src/Tools/jEdit/lib/Tools/jedit	Thu Sep 01 11:53:07 2016 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Sep 02 08:54:46 2016 +0200
@@ -42,6 +42,7 @@
   "src/jedit_options.scala"
   "src/jedit_resources.scala"
   "src/jedit_sessions.scala"
+  "src/keymap_merge.scala"
   "src/monitor_dockable.scala"
   "src/output_dockable.scala"
   "src/pide_docking_framework.scala"
--- a/src/Tools/jEdit/src/actions.xml	Thu Sep 01 11:53:07 2016 +0200
+++ b/src/Tools/jEdit/src/actions.xml	Fri Sep 02 08:54:46 2016 +0200
@@ -152,4 +152,9 @@
 	    isabelle.jedit.Isabelle.plugin_options(view);
 	  </CODE>
 	</ACTION>
+	<ACTION NAME="isabelle.keymap-merge">
+	  <CODE>
+	    isabelle.jedit.Keymap_Merge.check_dialog(view);
+	  </CODE>
+	</ACTION>
 </ACTIONS>
--- a/src/Tools/jEdit/src/jEdit.props	Thu Sep 01 11:53:07 2016 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Fri Sep 02 08:54:46 2016 +0200
@@ -177,6 +177,7 @@
 encodingDetectors=BOM XML-PI buffer-local-property
 end.shortcut=
 expand-abbrev.shortcut2=CA+SPACE
+expand-folds.shortcut=
 fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
 firstTime=false
 focus-buffer-switcher.shortcut2=A+CIRCUMFLEX
@@ -184,7 +185,7 @@
 gatchan.highlight.overview=false
 home.shortcut=
 insert-newline-indent.shortcut=
-insert-newline.shortcut=ENTER
+insert-newline.shortcut=
 isabelle-debugger.dock-position=floating
 isabelle-documentation.dock-position=right
 isabelle-output.dock-position=bottom
@@ -249,6 +250,11 @@
 match-bracket.shortcut2=C+9
 navigator.showOnToolbar=true
 next-bracket.shortcut2=C+e C+9
+options.shortcuts.deletekeymap.label=Delete
+options.shortcuts.duplicatekeymap.dialog.title=Keymap name
+options.shortcuts.duplicatekeymap.label=Duplicate
+options.shortcuts.resetkeymap.dialog.title=Reset keymap
+options.shortcuts.resetkeymap.label=Reset
 options.textarea.lineSpacing=-2
 plugin-blacklist.MacOSX.jar=true
 plugin.MacOSXPlugin.altDispatcher=false
@@ -281,6 +287,10 @@
 vfs.favorite.0=$ISABELLE_HOME
 vfs.favorite.1.type=1
 vfs.favorite.1=$ISABELLE_HOME_USER
+vfs.favorite.2.type=1
+vfs.favorite.2=$JEDIT_HOME
+vfs.favorite.3.type=1
+vfs.favorite.3=$JEDIT_SETTINGS
 view.antiAlias=standard
 view.blockCaret=true
 view.caretBlink=false
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/keymap_merge.scala	Fri Sep 02 08:54:46 2016 +0200
@@ -0,0 +1,262 @@
+/*  Title:      Tools/jEdit/src/keymap_merge.scala
+    Author:     Makarius
+
+Merge of Isabelle shortcuts vs. jEdit keymap.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.lang.{Class, Boolean => JBoolean}
+import java.awt.{Color, Dimension, BorderLayout}
+import javax.swing.{JPanel, JTable, JScrollPane, JOptionPane}
+import javax.swing.table.AbstractTableModel
+
+import scala.collection.JavaConversions
+
+import org.gjt.sp.jedit.{jEdit, View, GUIUtilities}
+import org.jedit.keymap.{KeymapManager, Keymap}
+
+
+object Keymap_Merge
+{
+  /** shortcuts **/
+
+  private def is_shortcut(property: String): Boolean =
+    (property.endsWith(".shortcut") || property.endsWith(".shortcut2")) &&
+    !property.startsWith("options.shortcuts.")
+
+  class Shortcut(val property: String, val binding: String)
+  {
+    override def toString: String = property + "=" + binding
+
+    def primary: Boolean = property.endsWith(".shortcut")
+
+    val action: String =
+      Library.try_unsuffix(".shortcut", property) orElse
+      Library.try_unsuffix(".shortcut2", property) getOrElse
+      error("Bad shortcut property: " + quote(property))
+
+    val label: String =
+      GUIUtilities.prettifyMenuLabel(jEdit.getProperty(action + ".label", ""))
+
+
+    /* ignore wrt. keymap */
+
+    private def prop_ignore: String = property + ".ignore"
+
+    def ignored_keymaps(): List[String] =
+      Library.space_explode(',', jEdit.getProperty(prop_ignore, ""))
+
+    def is_ignored(keymap_name: String): Boolean =
+      ignored_keymaps().contains(keymap_name)
+
+    def ignore(keymap_name: String)
+    {
+      val keymaps1 = Library.insert(keymap_name)(ignored_keymaps()).sorted
+      if (keymaps1.isEmpty) jEdit.resetProperty(prop_ignore)
+      else jEdit.setProperty(prop_ignore, keymaps1.mkString(","))
+    }
+
+    def set(keymap: Keymap): Unit = keymap.setShortcut(property, binding)
+    def reset(keymap: Keymap): Unit = keymap.setShortcut(property, null)
+  }
+
+
+  /* content wrt. keymap */
+
+  def convert_properties(props: java.util.Properties): List[Shortcut] =
+    if (props == null) Nil
+    else {
+      var result = List.empty[Shortcut]
+      for (entry <- JavaConversions.mapAsScalaMap(props)) {
+        entry match {
+          case (a: String, b: String) if is_shortcut(a) =>
+            result ::= new Shortcut(a, b)
+          case _ =>
+        }
+      }
+      result.sortBy(_.property)
+    }
+
+  def get_shortcut_conflicts(keymap_name: String, keymap: Keymap): List[(Shortcut, List[Shortcut])] =
+  {
+    val keymap_shortcuts =
+      if (keymap == null) Nil
+      else convert_properties(Untyped.get[java.util.Properties](keymap, "props"))
+
+    for (s <- convert_properties(jEdit.getProperties) if !s.is_ignored(keymap_name)) yield {
+      val conflicts =
+        keymap_shortcuts.filter(s1 =>
+          s.property == s1.property && s.binding != s1.binding ||
+          s.property != s1.property && s.binding == s1.binding && s1.binding != "")
+      (s, conflicts)
+    }
+  }
+
+
+
+  /** table **/
+
+  private def conflict_color: Color =
+    PIDE.options.color_value("error_color")
+
+  private sealed case class Table_Entry(shortcut: Shortcut, head: Option[Int], tail: List[Int])
+  {
+    override def toString: String =
+      if (head.isEmpty) "<html>" + HTML.output(shortcut.toString) + "</html>"
+      else
+        "<html><font style='color: #" + Color_Value.print(conflict_color) + ";'>" +
+          HTML.output("--- " + shortcut.toString) +
+        "</font></html>"
+  }
+
+  private class Table_Model(entries: List[Table_Entry]) extends AbstractTableModel
+  {
+    private val entries_count = entries.length
+    private def has_entry(row: Int): Boolean = 0 <= row && row <= entries_count
+    private def get_entry(row: Int): Option[Table_Entry] =
+      if (has_entry(row)) Some(entries(row)) else None
+
+    private val selected =
+      Synchronized[Set[Int]](
+        (for ((e, i) <- entries.iterator.zipWithIndex if e.head.isEmpty) yield i).toSet)
+
+    private def is_selected(row: Int): Boolean =
+      selected.value.contains(row)
+
+    private def select(head: Int, tail: List[Int], b: Boolean): Unit =
+      selected.change(set => if (b) set + head -- tail else set - head ++ tail)
+
+    def apply(keymap_name: String, keymap: Keymap)
+    {
+      GUI_Thread.require {}
+
+      for ((entry, row) <- entries.iterator.zipWithIndex if entry.head.isEmpty) {
+        val b = is_selected(row)
+        if (b) {
+          entry.tail.foreach(i => entries(i).shortcut.reset(keymap))
+          entry.shortcut.set(keymap)
+        }
+        else
+          entry.shortcut.ignore(keymap_name)
+      }
+    }
+
+    override def getColumnCount: Int = 2
+
+    override def getColumnClass(i: Int): Class[_ <: Object] =
+      if (i == 0) classOf[JBoolean] else classOf[Object]
+
+    override def getColumnName(i: Int): String =
+      if (i == 0) " " else if (i == 1) "Keyboard shortcut" else "???"
+
+    override def getRowCount: Int = entries_count
+
+    override def getValueAt(row: Int, column: Int): AnyRef =
+    {
+      get_entry(row) match {
+        case Some(entry) if column == 0 => JBoolean.valueOf(is_selected(row))
+        case Some(entry) if column == 1 => entry
+        case _ => null
+      }
+    }
+
+    override def isCellEditable(row: Int, column: Int): Boolean =
+      has_entry(row) && column == 0
+
+    override def setValueAt(value: AnyRef, row: Int, column: Int)
+    {
+      value match {
+        case obj: JBoolean if has_entry(row) && column == 0 =>
+          val b = obj.booleanValue
+          val entry = entries(row)
+          entry.head match {
+            case None => select(row, entry.tail, b)
+            case Some(head_row) =>
+              val head_entry = entries(head_row)
+              select(head_row, head_entry.tail, !b)
+          }
+          GUI_Thread.later { fireTableDataChanged() }
+        case _ =>
+      }
+    }
+  }
+
+  private class Table(table_model: Table_Model) extends JPanel(new BorderLayout)
+  {
+    private val cell_size = GUIUtilities.defaultTableCellSize()
+    private val table_size = new Dimension(cell_size.width * 2, cell_size.height * 15)
+
+    val table = new JTable(table_model)
+    table.setShowGrid(false)
+    table.setIntercellSpacing(new Dimension(0, 0))
+    table.setRowHeight(cell_size.height + 2)
+    table.setPreferredScrollableViewportSize(table_size)
+    table.setFillsViewportHeight(true)
+    table.getTableHeader.setReorderingAllowed(false)
+
+		table.getColumnModel.getColumn(0).setPreferredWidth(30)
+		table.getColumnModel.getColumn(0).setMinWidth(30)
+		table.getColumnModel.getColumn(0).setMaxWidth(30)
+		table.getColumnModel.getColumn(0).setResizable(false)
+		table.getColumnModel.getColumn(1).setPreferredWidth(table_size.width - 30)
+
+    val scroller = new JScrollPane(table)
+		scroller.getViewport.setBackground(table.getBackground)
+		scroller.setPreferredSize(table_size)
+
+    add(scroller, BorderLayout.CENTER)
+  }
+
+
+
+  /** check with optional dialog **/
+
+  def check_dialog(view: View)
+  {
+    GUI_Thread.require {}
+
+    val keymap_manager = jEdit.getKeymapManager
+    val keymap_name = jEdit.getProperty("keymap.current", KeymapManager.DEFAULT_KEYMAP_NAME)
+    val keymap =
+      keymap_manager.getKeymap(keymap_name) match {
+        case null => keymap_manager.getKeymap(KeymapManager.DEFAULT_KEYMAP_NAME)
+        case keymap => keymap
+      }
+
+    val all_shortcut_conflicts = get_shortcut_conflicts(keymap_name, keymap)
+    val no_shortcut_conflicts = for ((s, cs) <- all_shortcut_conflicts if cs.isEmpty) yield s
+    val shortcut_conflicts = all_shortcut_conflicts.filter(_._2.nonEmpty)
+
+    val table_entries =
+      for {
+        ((shortcut, conflicts), i) <- shortcut_conflicts zip
+          shortcut_conflicts.scanLeft(0)({ case (i, (_, cs)) => i + 1 + cs.length })
+        entry <-
+          Table_Entry(shortcut, None, ((i + 1) to (i + conflicts.length)).toList) ::
+          conflicts.map(Table_Entry(_, Some(i), Nil))
+      } yield entry
+
+    val table_model = new Table_Model(table_entries)
+
+    if (table_entries.nonEmpty &&
+        GUI.confirm_dialog(view,
+          "Pending Isabelle/jEdit keymap changes",
+          JOptionPane.OK_CANCEL_OPTION,
+          "The following Isabelle keymap changes are in conflict with the current",
+          "jEdit keymap " + quote(keymap_name) + ":",
+          new Table(table_model),
+          "Selected shortcuts will be applied, unselected changes will be ignored.",
+          "Results are stored in $JEDIT_SETTINGS/properties and $JEDIT_SETTINGS/keymaps/.") == 0)
+    { table_model.apply(keymap_name, keymap) }
+
+    no_shortcut_conflicts.foreach(_.set(keymap))
+
+    keymap.save()
+    keymap_manager.reload()
+    jEdit.saveSettings()
+  }
+}
--- a/src/Tools/jEdit/src/plugin.scala	Thu Sep 01 11:53:07 2016 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Sep 02 08:54:46 2016 +0200
@@ -335,6 +335,8 @@
 
           Session_Build.session_build(jEdit.getActiveView())
 
+          Keymap_Merge.check_dialog(jEdit.getActiveView())
+
         case msg: BufferUpdate
         if msg.getWhat == BufferUpdate.LOADED ||
           msg.getWhat == BufferUpdate.PROPERTIES_CHANGED ||
isabelle