--- a/Admin/components/components.sha1 Fri Aug 12 18:08:40 2016 +0200
+++ b/Admin/components/components.sha1 Fri Aug 12 20:58:20 2016 +0200
@@ -46,6 +46,7 @@
1f004a6bf20088a7e8f1b3d4153aa85de6fc1091 isabelle_fonts-20160101.tar.gz
379d51ef3b71452dac34ba905def3daa8b590f2e isabelle_fonts-20160102.tar.gz
878536aab1eaf1a52da560c20bb41ab942971fa3 isabelle_fonts-20160227.tar.gz
+9283e3b0b4c7239f57b18e076ec8bb21021832cb isabelle_fonts-20160812.tar.gz
8d83e433c1419e0c0cc5fd1762903d11b4a5752c jdk-6u31.tar.gz
38d2d2a91c66714c18430e136e7e5191af3996e6 jdk-7u11.tar.gz
d765bc4ad2f34d494429b2a8c1563c49db224944 jdk-7u13.tar.gz
@@ -60,6 +61,7 @@
d980055694ddfae430ee001c7ee877d535e97252 jdk-7u76.tar.gz
baa6de37bb6f7a104ce5fe6506bca3d2572d601a jdk-7u80.tar.gz
7d5b152ac70f720bb9e783fa45ecadcf95069584 jdk-7u9.tar.gz
+baf275a68d3f799a841932e4e9a95a1a604058ae jdk-8u102.tar.gz
5442f1015a0657259be0590b04572cd933431df7 jdk-8u11.tar.gz
cfecb1383faaf027ffbabfcd77a0b6a6521e0969 jdk-8u20.tar.gz
44ffeeae219782d40ce6822b580e608e72fd4c76 jdk-8u31.tar.gz
--- a/Admin/components/main Fri Aug 12 18:08:40 2016 +0200
+++ b/Admin/components/main Fri Aug 12 20:58:20 2016 +0200
@@ -4,7 +4,7 @@
cvc4-1.5pre-3
e-1.8
Haskabelle-2015
-isabelle_fonts-20160227
+isabelle_fonts-20160812
jdk-8u102
jedit_build-20160330
jfreechart-1.0.14-1
--- a/NEWS Fri Aug 12 18:08:40 2016 +0200
+++ b/NEWS Fri Aug 12 20:58:20 2016 +0200
@@ -136,6 +136,16 @@
before. The theory syntax for 'keywords' has been simplified
accordingly: optional abbrevs need to go into the new 'abbrevs' section.
+* ML and document antiquotations for file-systems paths are more uniform
+and diverse:
+
+ @{path NAME} -- no file-system check
+ @{file NAME} -- check for plain file
+ @{dir NAME} -- check for directory
+
+Minor INCOMPATIBILITY, former uses of @{file} and @{file_unchecked} may
+have to be changed.
+
*** Isar ***
@@ -624,6 +634,9 @@
*** ML ***
+* ML antiquotation @{path} is superseded by @{file}, which ensures that
+the argument is a plain file. Minor INCOMPATIBILITY.
+
* Integer.gcd and Integer.lcm use efficient operations from the Poly/ML
library (notably for big integers). Subtle change of semantics:
Integer.gcd and Integer.lcm both normalize the sign, results are never
--- a/etc/symbols Fri Aug 12 18:08:40 2016 +0200
+++ b/etc/symbols Fri Aug 12 20:58:20 2016 +0200
@@ -381,3 +381,7 @@
\<^esub> code: 0x0021d9 group: control_block font: IsabelleText abbrev: =_)
\<^bsup> code: 0x0021d7 group: control_block font: IsabelleText abbrev: =^(
\<^esup> code: 0x0021d6 group: control_block font: IsabelleText abbrev: =^)
+\<^file> code: 0x01F5CF group: icon font: IsabelleText
+\<^dir> code: 0x01F5C0 group: icon font: IsabelleText
+\<^url> code: 0x01F310 group: icon font: IsabelleText
+\<^doc> code: 0x01F4D3 group: icon font: IsabelleText
--- a/lib/fonts/IsabelleText.sfd Fri Aug 12 18:08:40 2016 +0200
+++ b/lib/fonts/IsabelleText.sfd Fri Aug 12 20:58:20 2016 +0200
@@ -19,7 +19,7 @@
OS2_WeightWidthSlopeOnly: 0
OS2_UseTypoMetrics: 1
CreationTime: 1050361371
-ModificationTime: 1456601690
+ModificationTime: 1471012141
PfmFamily: 17
TTFWeight: 400
TTFWidth: 5
@@ -2241,11 +2241,11 @@
DisplaySize: -96
AntiAlias: 1
FitToEm: 1
-WinInfo: 9504 18 16
+WinInfo: 128340 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 1404
+BeginChars: 1114189 1408
StartChar: u10000
Encoding: 65536 65536 0
@@ -31234,24 +31234,24 @@
1656 -203 1656 -203 1739.5 -116.5 c 128,-1,30
1823 -30 1823 -30 1881 73.5 c 128,-1,31
1939 177 1939 177 1972 301 c 128,-1,32
- 2005 425 2005 425 2005 555 c 0,33,34
- 2005 685 2005 685 1972.5 808 c 128,-1,35
- 1940 931 1940 931 1882 1034.5 c 128,-1,36
- 1824 1138 1824 1138 1741.5 1225 c 128,-1,37
- 1659 1312 1659 1312 1560.5 1372.5 c 128,-1,38
- 1462 1433 1462 1433 1346 1467 c 128,-1,39
- 1230 1501 1230 1501 1108 1501 c 0,40,41
- 988 1501 988 1501 873 1467.5 c 128,-1,42
- 758 1434 758 1434 659.5 1373.5 c 128,-1,43
- 561 1313 561 1313 478 1226.5 c 128,-1,44
- 395 1140 395 1140 336.5 1036.5 c 128,-1,45
- 278 933 278 933 245.5 809 c 128,-1,46
- 213 685 213 685 213 555 c 0,47,48
- 213 425 213 425 245.5 302 c 128,-1,49
- 278 179 278 179 335.5 75.5 c 128,-1,50
- 393 -28 393 -28 476 -115 c 128,-1,51
- 559 -202 559 -202 657.5 -262.5 c 128,-1,52
- 756 -323 756 -323 872 -357 c 128,-1,53
+ 2005 425 2005 425 2005 555 c 128,-1,33
+ 2005 685 2005 685 1972.5 808 c 128,-1,34
+ 1940 931 1940 931 1882 1034.5 c 128,-1,35
+ 1824 1138 1824 1138 1741.5 1225 c 128,-1,36
+ 1659 1312 1659 1312 1560.5 1372.5 c 128,-1,37
+ 1462 1433 1462 1433 1346 1467 c 128,-1,38
+ 1230 1501 1230 1501 1108 1501 c 0,39,40
+ 988 1501 988 1501 873 1467.5 c 128,-1,41
+ 758 1434 758 1434 659.5 1373.5 c 128,-1,42
+ 561 1313 561 1313 478 1226.5 c 128,-1,43
+ 395 1140 395 1140 336.5 1036.5 c 128,-1,44
+ 278 933 278 933 245.5 809 c 128,-1,45
+ 213 685 213 685 213 555 c 128,-1,46
+ 213 425 213 425 245.5 302 c 128,-1,47
+ 278 179 278 179 335.5 75.5 c 128,-1,48
+ 393 -28 393 -28 476 -115 c 128,-1,49
+ 559 -202 559 -202 657.5 -262.5 c 128,-1,50
+ 756 -323 756 -323 872 -357 c 128,-1,51
988 -391 988 -391 1110 -391 c 0,26,27
EndSplineSet
Validated: 1
@@ -62473,5 +62473,279 @@
724 -129 724 -129 864 -129 c 0,20,21
EndSplineSet
EndChar
+
+StartChar: u1F5CF
+Encoding: 128463 128463 1404
+Width: 1316
+VWidth: 1663
+Flags: W
+HStem: 97.7197 92<268.881 1047.12> 250.6 92<342.359 973.641> 438.76 92<342.359 973.641> 626.92 92<342.359 973.641> 815.08 92<342.359 973.641> 1003.24 92<342.359 973.641> 1191.4 92<342.359 973.641> 1344.28 92<268.881 1047.12>
+VStem: 176.881 92<189.72 1344.28> 342.359 631.281<250.6 342.6 438.76 530.76 626.92 718.92 815.08 907.08 1003.24 1095.24 1191.4 1283.4> 1047.12 92<189.72 1344.28>
+CounterMasks: 1 00e0
+LayerCount: 2
+Fore
+SplineSet
+1139.12 97.7197 m 1,0,-1
+ 176.881 97.7197 l 1,1,-1
+ 176.881 1436.28 l 1,2,-1
+ 1139.12 1436.28 l 1,3,-1
+ 1139.12 97.7197 l 1,0,-1
+1047.12 189.72 m 1,4,-1
+ 1047.12 1344.28 l 1,5,-1
+ 268.881 1344.28 l 1,6,-1
+ 268.881 189.72 l 1,7,-1
+ 1047.12 189.72 l 1,4,-1
+973.641 1191.4 m 1,8,-1
+ 342.359 1191.4 l 1,9,-1
+ 342.359 1283.4 l 1,10,-1
+ 973.641 1283.4 l 1,11,-1
+ 973.641 1191.4 l 1,8,-1
+973.641 1003.24 m 1,12,-1
+ 342.359 1003.24 l 1,13,-1
+ 342.359 1095.24 l 1,14,-1
+ 973.641 1095.24 l 1,15,-1
+ 973.641 1003.24 l 1,12,-1
+973.641 815.08 m 1,16,-1
+ 342.359 815.08 l 1,17,-1
+ 342.359 907.08 l 1,18,-1
+ 973.641 907.08 l 1,19,-1
+ 973.641 815.08 l 1,16,-1
+973.641 626.92 m 1,20,-1
+ 342.359 626.92 l 1,21,-1
+ 342.359 718.92 l 1,22,-1
+ 973.641 718.92 l 1,23,-1
+ 973.641 626.92 l 1,20,-1
+973.641 438.76 m 1,24,-1
+ 342.359 438.76 l 1,25,-1
+ 342.359 530.76 l 1,26,-1
+ 973.641 530.76 l 1,27,-1
+ 973.641 438.76 l 1,24,-1
+973.641 250.6 m 1,28,-1
+ 342.359 250.6 l 1,29,-1
+ 342.359 342.6 l 1,30,-1
+ 973.641 342.6 l 1,31,-1
+ 973.641 250.6 l 1,28,-1
+EndSplineSet
+EndChar
+
+StartChar: u1F4D3
+Encoding: 128211 128211 1405
+Width: 1064
+VWidth: 1762
+Flags: W
+HStem: 70.75 113.7<258.8 847.9> 751.15 78<409.3 704.4> 1004.55 78<409.3 704.4> 1148.05 112.3<552.118 720.5 832.1 847.9>
+VStem: 102.4 156.399<184.45 1148.05> 328.5 80.7998<829.15 1004.55> 704.4 80.7998<829.15 1004.55> 720.5 111.6<1260.35 1305.05> 847.9 113.699<184.45 1148.05>
+LayerCount: 2
+Fore
+SplineSet
+961.6 131.45 m 2,0,1
+ 961.6 113.078 961.6 113.078 941.787 92.194 c 0,2,3
+ 921.444 70.75 921.444 70.75 902.3 70.75 c 2,4,-1
+ 154.7 70.75 l 2,5,6
+ 149.31 70.75 149.31 70.75 144.938 71.698 c 128,-1,7
+ 140.566 72.6461 140.566 72.6461 136.496 75.4084 c 128,-1,8
+ 132.426 78.1707 132.426 78.1707 130.859 79.2896 c 128,-1,9
+ 129.293 80.4084 129.293 80.4084 125.173 84.775 c 128,-1,10
+ 121.053 89.1416 121.053 89.1416 120.921 89.2733 c 0,11,12
+ 120.071 90.1241 120.071 90.1241 117.082 92.9509 c 128,-1,13
+ 114.093 95.7776 114.093 95.7776 112.733 97.203 c 128,-1,14
+ 111.374 98.6284 111.374 98.6284 108.988 101.775 c 128,-1,15
+ 106.602 104.921 106.602 104.921 105.459 107.628 c 128,-1,16
+ 104.317 110.334 104.317 110.334 103.359 114.426 c 128,-1,17
+ 102.4 118.517 102.4 118.517 102.4 123.05 c 2,18,-1
+ 102.4 1202.45 l 2,19,20
+ 102.4 1234.63 102.4 1234.63 130.589 1257.6 c 0,21,22
+ 136.172 1262.06 136.172 1262.06 149.627 1267.2 c 128,-1,23
+ 163.083 1272.33 163.083 1272.33 192.782 1280.66 c 128,-1,24
+ 222.482 1288.98 222.482 1288.98 250.492 1296.33 c 128,-1,25
+ 278.501 1303.67 278.501 1303.67 336.958 1318.88 c 128,-1,26
+ 395.414 1334.08 395.414 1334.08 442.617 1346.66 c 0,27,28
+ 741.511 1426.25 741.511 1426.25 765.1 1426.25 c 0,29,30
+ 804.524 1426.25 804.524 1426.25 821.67 1403.62 c 0,31,32
+ 832.1 1389.85 832.1 1389.85 832.1 1370.45 c 2,33,-1
+ 832.1 1259.65 l 1,34,-1
+ 919.1 1259.65 l 2,35,36
+ 938.501 1259.65 938.501 1259.65 951.807 1238.52 c 0,37,38
+ 961.6 1222.96 961.6 1222.96 961.6 1210.15 c 2,39,-1
+ 961.6 131.45 l 2,0,1
+720.5 1260.35 m 1,40,-1
+ 720.5 1305.05 l 1,41,-1
+ 552.118 1260.35 l 1,42,-1
+ 720.5 1260.35 l 1,40,-1
+847.9 184.45 m 1,43,-1
+ 847.9 1148.05 l 1,44,-1
+ 258.8 1148.05 l 1,45,-1
+ 258.8 184.45 l 1,46,-1
+ 847.9 184.45 l 1,43,-1
+785.2 751.15 m 1,47,-1
+ 328.5 751.15 l 1,48,-1
+ 328.5 1082.55 l 1,49,-1
+ 785.2 1082.55 l 1,50,-1
+ 785.2 751.15 l 1,47,-1
+704.4 829.15 m 1,51,-1
+ 704.4 1004.55 l 1,52,-1
+ 409.3 1004.55 l 1,53,-1
+ 409.3 829.15 l 1,54,-1
+ 704.4 829.15 l 1,51,-1
+EndSplineSet
+EndChar
+
+StartChar: u1F310
+Encoding: 127760 127760 1406
+Width: 1688
+VWidth: 1788
+Flags: W
+HStem: 20.2002 91.7907<761.056 798 889.3 926.891> 425.087 91.63<626.537 798 889.3 1061.42> 716 91.2998<194.002 451.735 539.764 798 889.3 1148.24 1236.27 1494> 1007.28 91.6301<626.532 798 889.3 1061.42> 1412.01 91.7906<761.105 798 889.3 926.94>
+VStem: 102.2 91.8017<519.669 716 807.3 1004.44> 448.309 91.4551<486.943 716 807.3 1037.01> 798 91.2998<111.991 425.087 511.895 716 807.3 1012.11 1098.91 1412.01> 1148.24 91.455<486.937 716 807.3 1036.95> 1494 91.7974<519.351 716 807.3 1004.11>
+LayerCount: 2
+Fore
+SplineSet
+1585.8 762 m 128,-1,1
+ 1585.8 454.831 1585.8 454.831 1368.48 237.523 c 128,-1,2
+ 1151.14 20.2002 1151.14 20.2002 844 20.2002 c 128,-1,3
+ 536.84 20.2002 536.84 20.2002 319.523 237.523 c 128,-1,4
+ 102.2 454.85 102.2 454.85 102.2 762 c 128,-1,5
+ 102.2 1069.14 102.2 1069.14 319.523 1286.48 c 128,-1,6
+ 536.826 1503.8 536.826 1503.8 844 1503.8 c 128,-1,7
+ 1151.16 1503.8 1151.16 1503.8 1368.48 1286.48 c 128,-1,0
+ 1585.8 1069.16 1585.8 1069.16 1585.8 762 c 128,-1,1
+1262.08 1260.78 m 1,8,9
+ 1167.74 1340.05 1167.74 1340.05 1053.44 1378.52 c 1,10,11
+ 1107.7 1285.5 1107.7 1285.5 1148.82 1184.39 c 1,12,13
+ 1209.39 1218.15 1209.39 1218.15 1262.08 1260.78 c 1,8,9
+1494 807.3 m 1,14,15
+ 1479.42 1030.47 1479.42 1030.47 1328.63 1197.13 c 1,16,17
+ 1261.15 1140.95 1261.15 1140.95 1181.23 1098.32 c 1,18,19
+ 1232.11 945.833 1232.11 945.833 1239.7 807.3 c 1,20,-1
+ 1494 807.3 l 1,14,15
+1066.08 1144.97 m 1,21,22
+ 1009.85 1286.26 1009.85 1286.26 927.548 1408.03 c 1,23,24
+ 908.07 1410.67 908.07 1410.67 889.3 1412.04 c 1,25,-1
+ 889.3 1098.9 l 1,26,27
+ 975.008 1107.19 975.008 1107.19 1066.08 1144.97 c 1,21,22
+798 1098.91 m 1,28,-1
+ 798 1412.01 l 1,29,30
+ 779.771 1410.65 779.771 1410.65 760.503 1408.04 c 1,31,32
+ 678.789 1286.3 678.789 1286.3 621.993 1144.94 c 1,33,34
+ 712.892 1107.2 712.892 1107.2 798 1098.91 c 1,28,-1
+1148.24 807.3 m 1,35,36
+ 1140.79 926.069 1140.79 926.069 1097.73 1058.8 c 1,37,38
+ 991.801 1015.61 991.801 1015.61 889.3 1007.27 c 1,39,-1
+ 889.3 807.3 l 1,40,-1
+ 1148.24 807.3 l 1,35,36
+1494 716 m 1,41,-1
+ 1239.69 716 l 1,42,43
+ 1232.09 578.093 1232.09 578.093 1181.2 425.582 c 1,44,45
+ 1261.15 382.472 1261.15 382.472 1328.59 326.768 c 1,46,47
+ 1479.43 492.879 1479.43 492.879 1494 716 c 1,41,-1
+634.728 1378.57 m 1,48,49
+ 520.263 1340.05 520.263 1340.05 425.925 1260.78 c 1,50,51
+ 478.599 1218.16 478.599 1218.16 539.218 1184.36 c 1,52,53
+ 580.313 1285.02 580.313 1285.02 634.728 1378.57 c 1,48,49
+798 807.3 m 1,54,-1
+ 798 1007.28 l 1,55,56
+ 696.095 1015.61 696.095 1015.61 590.27 1058.8 c 1,57,58
+ 547.2 926.041 547.2 926.041 539.757 807.3 c 1,59,-1
+ 798 807.3 l 1,54,-1
+1148.24 716 m 1,60,-1
+ 889.3 716 l 1,61,-1
+ 889.3 516.727 l 1,62,63
+ 991.801 508.391 991.801 508.391 1097.73 465.201 c 1,64,65
+ 1140.78 597.834 1140.78 597.834 1148.24 716 c 1,60,-1
+1262.08 263.218 m 1,66,67
+ 1209.39 305.845 1209.39 305.845 1148.78 339.635 c 1,68,69
+ 1107.69 239.016 1107.69 239.016 1053.27 145.428 c 1,70,71
+ 1167.73 183.946 1167.73 183.946 1262.08 263.218 c 1,66,67
+506.805 1098.42 m 1,72,73
+ 426.835 1141.54 426.835 1141.54 359.408 1197.23 c 1,74,75
+ 208.571 1031.1 208.571 1031.1 193.993 807.3 c 1,76,-1
+ 448.304 807.3 l 1,77,78
+ 455.9 945.847 455.9 945.847 506.805 1098.42 c 1,72,73
+798 516.717 m 1,79,-1
+ 798 716 l 1,80,-1
+ 539.764 716 l 1,81,82
+ 547.211 597.894 547.211 597.894 590.269 465.204 c 1,83,84
+ 696.116 508.387 696.116 508.387 798 516.717 c 1,79,-1
+1066.01 379.06 m 1,85,86
+ 975.034 416.801 975.034 416.801 889.3 425.102 c 1,87,-1
+ 889.3 111.961 l 1,88,89
+ 908.073 113.327 908.073 113.327 927.498 115.963 c 1,90,91
+ 1009.22 237.715 1009.22 237.715 1066.01 379.06 c 1,85,86
+798 111.991 m 1,92,-1
+ 798 425.087 l 1,93,94
+ 712.91 416.803 712.91 416.803 621.915 379.03 c 1,95,96
+ 678.161 237.718 678.161 237.718 760.453 115.968 c 1,97,98
+ 779.756 113.346 779.756 113.346 798 111.991 c 1,92,-1
+506.804 425.582 m 1,99,100
+ 455.912 578.112 455.912 578.112 448.309 716 c 1,101,-1
+ 194.002 716 l 1,102,103
+ 208.584 493.507 208.584 493.507 359.439 326.795 c 1,104,105
+ 426.844 382.467 426.844 382.467 506.804 425.582 c 1,99,100
+634.728 145.428 m 1,106,107
+ 580.299 239.015 580.299 239.015 539.218 339.635 c 1,108,109
+ 478.599 305.837 478.599 305.837 425.925 263.219 c 1,110,111
+ 520.274 183.946 520.274 183.946 634.728 145.428 c 1,106,107
+EndSplineSet
+EndChar
+
+StartChar: u1F5C0
+Encoding: 128448 128448 1407
+Width: 1158
+VWidth: 1805
+Flags: W
+VStem: 102.5 106.7<602.301 1215.44> 841 106.7<238.4 843.752> 949.5 106<214.643 1065.52>
+LayerCount: 2
+Fore
+SplineSet
+1055.5 163.65 m 2,0,1
+ 1055.5 136.806 1055.5 136.806 1027.85 118.777 c 0,2,3
+ 1022.2 115.241 1022.2 115.241 1014.76 112.968 c 128,-1,4
+ 1007.33 110.694 1007.33 110.694 1002.34 109.835 c 128,-1,5
+ 997.355 108.975 997.355 108.975 982.41 107.168 c 128,-1,6
+ 967.465 105.361 967.465 105.361 959.394 104.238 c 0,7,8
+ 904.83 96.6504 904.83 96.6504 890.5 96.6504 c 0,9,10
+ 883.016 96.6504 883.016 96.6504 873.952 99.5816 c 128,-1,11
+ 864.889 102.513 864.889 102.513 849.994 110.465 c 128,-1,12
+ 835.1 118.417 835.1 118.417 822.385 125.88 c 128,-1,13
+ 809.67 133.343 809.67 133.343 783.12 149.187 c 128,-1,14
+ 756.569 165.032 756.569 165.032 735.957 176.967 c 0,15,16
+ 593.462 258.096 593.462 258.096 312.993 419.26 c 0,17,18
+ 271.572 443.835 271.572 443.835 190.566 491.606 c 1,19,20
+ 167.093 503.176 167.093 503.176 129.033 528.548 c 2,21,-1
+ 127.217 529.759 l 1,22,-1
+ 125.639 531.266 l 2,23,24
+ 102.5 553.353 102.5 553.353 102.5 580.15 c 2,25,-1
+ 102.5 1324.95 l 2,26,27
+ 102.5 1345.8 102.5 1345.8 118.02 1356.97 c 128,-1,28
+ 133.539 1368.15 133.539 1368.15 152.7 1368.15 c 0,29,30
+ 159.813 1368.15 159.813 1368.15 166.945 1365.85 c 128,-1,31
+ 174.078 1363.55 174.078 1363.55 178.378 1361.22 c 128,-1,32
+ 182.677 1358.89 182.677 1358.89 193.163 1352.3 c 128,-1,33
+ 203.649 1345.7 203.649 1345.7 209.454 1342.3 c 1,34,-1
+ 210.3 1409.11 l 2,35,36
+ 210.3 1429.22 210.3 1429.22 224.625 1441.93 c 128,-1,37
+ 238.95 1454.64 238.95 1454.64 258.424 1456.26 c 2,38,-1
+ 266.169 1456.91 l 1,39,-1
+ 694.479 1211.87 l 1,40,41
+ 737.3 1247.83 737.3 1247.83 771.289 1271.32 c 2,42,-1
+ 784.176 1280.22 l 1,43,-1
+ 1055.5 1126.73 l 1,44,-1
+ 1055.5 163.65 l 2,0,1
+949.5 214.858 m 1,45,-1
+ 949.5 1065.52 l 1,46,-1
+ 792.356 1156.34 l 1,47,-1
+ 699.305 1084.98 l 1,48,-1
+ 317 1304.2 l 1,49,-1
+ 317 1278.28 l 1,50,-1
+ 947.7 903.78 l 1,51,-1
+ 947.7 214.641 l 2,52,53
+ 948.335 214.717 948.335 214.717 949.5 214.858 c 1,45,-1
+841 238.4 m 1,54,-1
+ 841 843.752 l 1,55,-1
+ 209.2 1215.44 l 1,56,-1
+ 209.2 602.301 l 1,57,-1
+ 841 238.4 l 1,54,-1
+EndSplineSet
+EndChar
EndChars
EndSplineFont
--- a/lib/fonts/IsabelleTextBold.sfd Fri Aug 12 18:08:40 2016 +0200
+++ b/lib/fonts/IsabelleTextBold.sfd Fri Aug 12 20:58:20 2016 +0200
@@ -20,7 +20,7 @@
OS2_WeightWidthSlopeOnly: 0
OS2_UseTypoMetrics: 1
CreationTime: 1050374980
-ModificationTime: 1456601640
+ModificationTime: 1471012188
PfmFamily: 17
TTFWeight: 700
TTFWidth: 5
@@ -1678,10 +1678,10 @@
DisplaySize: -96
AntiAlias: 1
FitToEm: 1
-WinInfo: 9513 21 15
+WinInfo: 127638 21 15
BeginPrivate: 0
EndPrivate
-BeginChars: 1114115 1396
+BeginChars: 1114115 1400
StartChar: .notdef
Encoding: 1114112 -1 0
@@ -68852,5 +68852,270 @@
734 -78 734 -78 864 -78 c 0,20,21
EndSplineSet
EndChar
+
+StartChar: u1F310
+Encoding: 127760 127760 1396
+Width: 1688
+VWidth: 1788
+Flags: W
+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
+EndSplineSet
+EndChar
+
+StartChar: u1F4D3
+Encoding: 128211 128211 1397
+Width: 1064
+VWidth: 1762
+Flags: W
+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
+EndSplineSet
+EndChar
+
+StartChar: u1F5C0
+Encoding: 128448 128448 1398
+Width: 1158
+VWidth: 1805
+Flags: W
+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
+EndSplineSet
+EndChar
+
+StartChar: u1F5CF
+Encoding: 128463 128463 1399
+Width: 1316
+VWidth: 1663
+Flags: W
+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
+EndSplineSet
+EndChar
EndChars
EndSplineFont
--- a/lib/fonts/README Fri Aug 12 18:08:40 2016 +0200
+++ b/lib/fonts/README Fri Aug 12 20:58:20 2016 +0200
@@ -3,6 +3,10 @@
(free) fonts: Bluesky TeX fonts (scaled 222%) and Bitstream Vera Mono,
with some additions from DejaVu Sans Mono and DejaVu Sans.
+Some additional symbols are from Symbola. See http://greekfonts.teilar.gr
+"In lieu of a licence; fonts and documents in this site are free for any use;
+George Douros".
+
----------------------------------------------------------------------------
Computer Modern PostScript Fonts
--- a/lib/texinputs/isabellesym.sty Fri Aug 12 18:08:40 2016 +0200
+++ b/lib/texinputs/isabellesym.sty Fri Aug 12 20:58:20 2016 +0200
@@ -367,3 +367,6 @@
\newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}}
\newcommand{\isasymcomment}{\isatext{---}}
\newcommand{\isasymproof}{\isamath{\,\langle\mathit{proof}\rangle}}
+\newcommand{\isactrlundefined}{\isakeyword{undefined}\ }
+\newcommand{\isactrlfile}{\isakeyword{file}\ }
+\newcommand{\isactrldir}{\isakeyword{dir}\ }
--- a/src/Doc/Codegen/Adaptation.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/Codegen/Adaptation.thy Fri Aug 12 20:58:20 2016 +0200
@@ -154,7 +154,7 @@
The @{theory HOL} @{theory Main} theory already provides a code
generator setup which should be suitable for most applications.
Common extensions and modifications are available by certain
- theories in @{file "~~/src/HOL/Library"}; beside being useful in
+ theories in \<^dir>\<open>~~/src/HOL/Library\<close>; beside being useful in
applications, they may serve as a tutorial for customising the code
generator setup (see below \secref{sec:adaptation_mechanisms}).
--- a/src/Doc/Codegen/Evaluation.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/Codegen/Evaluation.thy Fri Aug 12 20:58:20 2016 +0200
@@ -340,7 +340,7 @@
For technical reasons it is sometimes necessary to separate
generation and compilation of code which is supposed to be used in
the system runtime. For this @{command code_reflect} with an
- optional @{text "file"} argument can be used:
+ optional \<^theory_text>\<open>file\<close> argument can be used:
\<close>
code_reflect %quote Rat
--- a/src/Doc/Codegen/Further.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/Codegen/Further.thy Fri Aug 12 20:58:20 2016 +0200
@@ -148,7 +148,7 @@
subsection \<open>Parallel computation\<close>
text \<open>
- Theory @{text Parallel} in @{file "~~/src/HOL/Library"} contains
+ Theory @{text Parallel} in \<^dir>\<open>~~/src/HOL/Library\<close> contains
operations to exploit parallelism inside the Isabelle/ML
runtime engine.
\<close>
--- a/src/Doc/Codegen/Inductive_Predicate.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/Codegen/Inductive_Predicate.thy Fri Aug 12 20:58:20 2016 +0200
@@ -262,7 +262,7 @@
text \<open>
Further examples for compiling inductive predicates can be found in
- @{file "~~/src/HOL/Predicate_Compile_Examples/Examples.thy"}. There are
+ \<^file>\<open>~~/src/HOL/Predicate_Compile_Examples/Examples.thy\<close>. There are
also some examples in the Archive of Formal Proofs, notably in the
@{text "POPLmark-deBruijn"} and the @{text "FeatherweightJava"}
sessions.
--- a/src/Doc/Corec/Corec.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/Corec/Corec.thy Fri Aug 12 20:58:20 2016 +0200
@@ -22,7 +22,7 @@
text \<open>
Isabelle's (co)datatype package @{cite "isabelle-datatypes"} offers a convenient
syntax for introducing codatatypes. For example, the type of (infinite) streams
-can be defined as follows (cf. @{file "~~/src/HOL/Library/Stream.thy"}):
+can be defined as follows (cf. \<^file>\<open>~~/src/HOL/Library/Stream.thy\<close>):
\<close>
codatatype 'a stream =
@@ -38,7 +38,7 @@
@{command corecursive}, @{command friend_of_corec}, and @{command coinduction_upto}.
It also covers the @{method corec_unique} proof method.
The package is not part of @{theory Main}; it is located in
-@{file "~~/src/HOL/Library/BNF_Corec.thy"}.
+\<^file>\<open>~~/src/HOL/Library/BNF_Corec.thy\<close>.
The @{command corec} command generalizes \keyw{primcorec} in three main
respects. First, it allows multiple constructors around corecursive calls, where
@@ -127,7 +127,7 @@
text \<open>
The package is illustrated through concrete examples featuring different flavors
of corecursion. More examples can be found in the directory
-@{file "~~/src/HOL/Corec_Examples"}.
+\<^dir>\<open>~~/src/HOL/Corec_Examples\<close>.
\<close>
@@ -368,7 +368,7 @@
text \<open>
A more elaborate case study, revolving around the filter function on lazy lists,
-is presented in @{file "~~/src/HOL/Corec_Examples/LFilter.thy"}.
+is presented in \<^file>\<open>~~/src/HOL/Corec_Examples/LFilter.thy\<close>.
\<close>
--- a/src/Doc/Datatypes/Datatypes.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Aug 12 20:58:20 2016 +0200
@@ -78,7 +78,7 @@
infinite branching.
The package is part of @{theory Main}. Additional functionality is provided by
-the theory @{file "~~/src/HOL/Library/BNF_Axiomatization.thy"}.
+the theory \<^file>\<open>~~/src/HOL/Library/BNF_Axiomatization.thy\<close>.
The package, like its predecessor, fully adheres to the LCF philosophy
@{cite mgordon79}: The characteristic theorems associated with the specified
@@ -163,7 +163,7 @@
text \<open>
Datatypes are illustrated through concrete examples featuring different flavors
of recursion. More examples can be found in the directory
-@{file "~~/src/HOL/Datatype_Examples"}.
+\<^dir>\<open>~~/src/HOL/Datatype_Examples\<close>.
\<close>
@@ -1138,7 +1138,7 @@
\label{sssec:datatype-compat}\<close>
text \<open>
-The theory @{file "~~/src/HOL/Library/Countable.thy"} provides a
+The theory \<^file>\<open>~~/src/HOL/Library/Countable.thy\<close> provides a
proof method called @{method countable_datatype} that can be used to prove the
countability of many datatypes, building on the countability of the types
appearing in their definitions and of any type arguments. For example:
@@ -1218,7 +1218,7 @@
\end{itemize}
The old command is still available as \keyw{old_datatype} in theory
-@{file "~~/src/HOL/Library/Old_Datatype.thy"}. However, there is no general
+\<^file>\<open>~~/src/HOL/Library/Old_Datatype.thy\<close>. However, there is no general
way to register old-style datatypes as new-style datatypes. If the objective
is to define new-style datatypes with nested recursion through old-style
datatypes, the old-style datatypes can be registered as a BNF
@@ -1247,7 +1247,7 @@
text \<open>
Primitive recursion is illustrated through concrete examples based on the
datatypes defined in Section~\ref{ssec:datatype-introductory-examples}. More
-examples can be found in the directory @{file "~~/src/HOL/Datatype_Examples"}.
+examples can be found in the directory \<^dir>\<open>~~/src/HOL/Datatype_Examples\<close>.
\<close>
@@ -1320,7 +1320,7 @@
Pattern matching is only available for the argument on which the recursion takes
place. Fortunately, it is easy to generate pattern-maching equations using the
@{command simps_of_case} command provided by the theory
-@{file "~~/src/HOL/Library/Simps_Case_Conv.thy"}.
+\<^file>\<open>~~/src/HOL/Library/Simps_Case_Conv.thy\<close>.
\<close>
simps_of_case at_simps_alt: at.simps
@@ -1760,7 +1760,7 @@
Codatatypes can be specified using the @{command codatatype} command. The
command is first illustrated through concrete examples featuring different
flavors of corecursion. More examples can be found in the directory
-@{file "~~/src/HOL/Datatype_Examples"}. The \emph{Archive of Formal Proofs} also
+\<^dir>\<open>~~/src/HOL/Datatype_Examples\<close>. The \emph{Archive of Formal Proofs} also
includes some useful codatatypes, notably for lazy lists @{cite
"lochbihler-2010"}.
\<close>
@@ -2038,7 +2038,7 @@
on @{command primcorec} and @{command primcorecursive}; \keyw{corec} and
\keyw{corecursive} are described in a separate tutorial
@{cite "isabelle-corec"}. More examples can be found in the directories
-@{file "~~/src/HOL/Datatype_Examples"} and @{file "~~/src/HOL/Corec_Examples"}.
+\<^dir>\<open>~~/src/HOL/Datatype_Examples\<close> and \<^dir>\<open>~~/src/HOL/Corec_Examples\<close>.
Whereas recursive functions consume datatypes one constructor at a time,
corecursive functions construct codatatypes one constructor at a time.
@@ -2082,7 +2082,7 @@
text \<open>
Primitive corecursion is illustrated through concrete examples based on the
codatatypes defined in Section~\ref{ssec:codatatype-introductory-examples}. More
-examples can be found in the directory @{file "~~/src/HOL/Datatype_Examples"}.
+examples can be found in the directory \<^dir>\<open>~~/src/HOL/Datatype_Examples\<close>.
The code view is favored in the examples below. Sections
\ref{ssec:primrec-constructor-view} and \ref{ssec:primrec-destructor-view}
present the same examples expressed using the constructor and destructor views.
@@ -2143,7 +2143,7 @@
Pattern matching is not supported by @{command primcorec}. Fortunately, it is
easy to generate pattern-maching equations using the @{command simps_of_case}
-command provided by the theory @{file "~~/src/HOL/Library/Simps_Case_Conv.thy"}.
+command provided by the theory \<^file>\<open>~~/src/HOL/Library/Simps_Case_Conv.thy\<close>.
\<close>
simps_of_case lapp_simps: lapp.code
@@ -2776,7 +2776,7 @@
text \<open>
The example below shows how to register a type as a BNF using the @{command bnf}
command. Some of the proof obligations are best viewed with the theory
-@{file "~~/src/HOL/Library/Cardinal_Notations.thy"} imported.
+\<^file>\<open>~~/src/HOL/Library/Cardinal_Notations.thy\<close> imported.
The type is simply a copy of the function space @{typ "'d \<Rightarrow> 'a"}, where @{typ 'a}
is live and @{typ 'd} is dead. We introduce it together with its map function,
@@ -2875,10 +2875,10 @@
This particular example does not need any nonemptiness witness, because the
one generated by default is good enough, but in general this would be
-necessary. See @{file "~~/src/HOL/Basic_BNFs.thy"},
-@{file "~~/src/HOL/Library/Countable_Set_Type.thy"},
-@{file "~~/src/HOL/Library/FSet.thy"}, and
-@{file "~~/src/HOL/Library/Multiset.thy"} for further examples of BNF
+necessary. See \<^file>\<open>~~/src/HOL/Basic_BNFs.thy\<close>,
+\<^file>\<open>~~/src/HOL/Library/Countable_Set_Type.thy\<close>,
+\<^file>\<open>~~/src/HOL/Library/FSet.thy\<close>, and
+\<^file>\<open>~~/src/HOL/Library/Multiset.thy\<close> for further examples of BNF
registration, some of which feature custom witnesses.
For many typedefs, lifting the BNF structure from the raw type to the abstract
@@ -3107,7 +3107,7 @@
The command is useful to reason abstractly about BNFs. The axioms are safe
because there exist BNFs of arbitrary large arities. Applications must import
-the @{file "~~/src/HOL/Library/BNF_Axiomatization.thy"} theory
+the \<^file>\<open>~~/src/HOL/Library/BNF_Axiomatization.thy\<close> theory
to use this functionality.
\<close>
@@ -3210,7 +3210,7 @@
\noindent
The @{command simps_of_case} command provided by theory
-@{file "~~/src/HOL/Library/Simps_Case_Conv.thy"} converts a single equation with
+\<^file>\<open>~~/src/HOL/Library/Simps_Case_Conv.thy\<close> converts a single equation with
a complex case expression on the right-hand side into a set of pattern-matching
equations. For example,
\<close>
@@ -3249,7 +3249,7 @@
\noindent
The \keyw{case_of_simps} command provided by theory
-@{file "~~/src/HOL/Library/Simps_Case_Conv.thy"} converts a set of
+\<^file>\<open>~~/src/HOL/Library/Simps_Case_Conv.thy\<close> converts a set of
pattern-matching equations into single equation with a complex case expression
on the right-hand side (cf.\ @{command simps_of_case}). For example,
\<close>
@@ -3386,7 +3386,7 @@
@{text "('a\<^sub>1 \<Rightarrow> nat) \<Rightarrow> \<dots> \<Rightarrow> ('a\<^sub>m \<Rightarrow> nat) \<Rightarrow> u \<Rightarrow> nat"} using
the ML function @{ML BNF_LFP_Size.register_size} or
@{ML BNF_LFP_Size.register_size_global}. See theory
-@{file "~~/src/HOL/Library/Multiset.thy"} for an example.
+\<^file>\<open>~~/src/HOL/Library/Multiset.thy\<close> for an example.
\<close>
--- a/src/Doc/Implementation/Eq.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/Implementation/Eq.thy Fri Aug 12 20:58:20 2016 +0200
@@ -64,10 +64,10 @@
@{index_ML Thm.equal_elim: "thm -> thm -> thm"} \\
\end{mldecls}
- See also @{file "~~/src/Pure/thm.ML" } for further description of these
- inference rules, and a few more for primitive \<open>\<beta>\<close> and \<open>\<eta>\<close> conversions. Note
- that \<open>\<alpha>\<close> conversion is implicit due to the representation of terms with
- de-Bruijn indices (\secref{sec:terms}).
+ See also \<^file>\<open>~~/src/Pure/thm.ML\<close> for further description of these inference
+ rules, and a few more for primitive \<open>\<beta>\<close> and \<open>\<eta>\<close> conversions. Note that \<open>\<alpha>\<close>
+ conversion is implicit due to the representation of terms with de-Bruijn
+ indices (\secref{sec:terms}).
\<close>
--- a/src/Doc/Implementation/Integration.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/Implementation/Integration.thy Fri Aug 12 20:58:20 2016 +0200
@@ -132,9 +132,9 @@
\<close>
text %mlex \<open>
- The file @{"file" "~~/src/HOL/ex/Commands.thy"} shows some example Isar
- command definitions, with the all-important theory header declarations for
- outer syntax keywords.
+ The file \<^file>\<open>~~/src/HOL/ex/Commands.thy\<close> shows some example Isar command
+ definitions, with the all-important theory header declarations for outer
+ syntax keywords.
\<close>
--- a/src/Doc/Implementation/Logic.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/Implementation/Logic.thy Fri Aug 12 20:58:20 2016 +0200
@@ -1248,11 +1248,11 @@
\<close>
text %mlex \<open>
- \<^item> @{file "~~/src/HOL/Proofs/ex/Proof_Terms.thy"} provides basic examples
- involving proof terms.
+ \<^item> \<^file>\<open>~~/src/HOL/Proofs/ex/Proof_Terms.thy\<close> provides basic examples involving
+ proof terms.
- \<^item> @{file "~~/src/HOL/Proofs/ex/XML_Data.thy"} demonstrates export and import
- of proof terms via XML/ML data representation.
+ \<^item> \<^file>\<open>~~/src/HOL/Proofs/ex/XML_Data.thy\<close> demonstrates export and import of
+ proof terms via XML/ML data representation.
\<close>
end
--- a/src/Doc/Implementation/ML.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/Implementation/ML.thy Fri Aug 12 20:58:20 2016 +0200
@@ -22,8 +22,8 @@
The main aspects of Isabelle/ML are introduced below. These first-hand
explanations should help to understand how proper Isabelle/ML is to be read
and written, and to get access to the wealth of experience that is expressed
- in the source text and its history of changes.\<^footnote>\<open>See @{url
- "http://isabelle.in.tum.de/repos/isabelle"} for the full Mercurial history.
+ in the source text and its history of changes.\<^footnote>\<open>See
+ \<^url>\<open>http://isabelle.in.tum.de/repos/isabelle\<close> for the full Mercurial history.
There are symbolic tags to refer to official Isabelle releases, as opposed
to arbitrary \<^emph>\<open>tip\<close> versions that merely reflect snapshots that are never
really up-to-date.\<close>
@@ -38,9 +38,8 @@
really going on and how things really work. This is a non-trivial aim, but
it is supported by a certain style of writing Isabelle/ML that has emerged
from long years of system development.\<^footnote>\<open>See also the interesting style guide
- for OCaml @{url
- "http://caml.inria.fr/resources/doc/guides/guidelines.en.html"} which shares
- many of our means and ends.\<close>
+ for OCaml \<^url>\<open>http://caml.inria.fr/resources/doc/guides/guidelines.en.html\<close>
+ which shares many of our means and ends.\<close>
The main principle behind any coding style is \<^emph>\<open>consistency\<close>. For a single
author of a small program this merely means ``choose your style and stick to
@@ -63,8 +62,8 @@
text \<open>
Isabelle source files have a certain standardized header format (with
precise spacing) that follows ancient traditions reaching back to the
- earliest versions of the system by Larry Paulson. See @{file
- "~~/src/Pure/thm.ML"}, for example.
+ earliest versions of the system by Larry Paulson. See
+ \<^file>\<open>~~/src/Pure/thm.ML\<close>, for example.
The header includes at least \<^verbatim>\<open>Title\<close> and \<^verbatim>\<open>Author\<close> entries, followed by a
prose description of the purpose of the module. The latter can range from a
@@ -1385,8 +1384,8 @@
32-bit Poly/ML, and much higher for 64-bit systems.\<close>
Structure @{ML_structure IntInf} of SML97 is obsolete and superseded by
- @{ML_structure Int}. Structure @{ML_structure Integer} in @{file
- "~~/src/Pure/General/integer.ML"} provides some additional operations.
+ @{ML_structure Int}. Structure @{ML_structure Integer} in
+ \<^file>\<open>~~/src/Pure/General/integer.ML\<close> provides some additional operations.
\<close>
@@ -1445,8 +1444,7 @@
text \<open>
Apart from @{ML Option.map} most other operations defined in structure
@{ML_structure Option} are alien to Isabelle/ML and never used. The
- operations shown above are defined in @{file
- "~~/src/Pure/General/basics.ML"}.
+ operations shown above are defined in \<^file>\<open>~~/src/Pure/General/basics.ML\<close>.
\<close>
@@ -1474,9 +1472,9 @@
is required.
\<^descr> @{ML member}, @{ML insert}, @{ML remove}, @{ML update} treat lists as a
- set-like container that maintains the order of elements. See @{file
- "~~/src/Pure/library.ML"} for the full specifications (written in ML). There
- are some further derived operations like @{ML union} or @{ML inter}.
+ set-like container that maintains the order of elements. See
+ \<^file>\<open>~~/src/Pure/library.ML\<close> for the full specifications (written in ML).
+ There are some further derived operations like @{ML union} or @{ML inter}.
Note that @{ML insert} is conservative about elements that are already a
@{ML member} of the list, while @{ML update} ensures that the latest entry
@@ -1518,8 +1516,8 @@
fold_rev} attempts to preserve the order of elements in the result.
This way of merging lists is typical for context data
- (\secref{sec:context-data}). See also @{ML merge} as defined in @{file
- "~~/src/Pure/library.ML"}.
+ (\secref{sec:context-data}). See also @{ML merge} as defined in
+ \<^file>\<open>~~/src/Pure/library.ML\<close>.
\<close>
@@ -1555,8 +1553,8 @@
Association lists are adequate as simple implementation of finite mappings
in many practical situations. A more advanced table structure is defined in
- @{file "~~/src/Pure/General/table.ML"}; that version scales easily to
- thousands or millions of elements.
+ \<^file>\<open>~~/src/Pure/General/table.ML\<close>; that version scales easily to thousands or
+ millions of elements.
\<close>
@@ -1782,8 +1780,7 @@
on the associated condition variable, and returns the result \<open>y\<close>.
There are some further variants of the @{ML Synchronized.guarded_access}
- combinator, see @{file "~~/src/Pure/Concurrent/synchronized.ML"} for
- details.
+ combinator, see \<^file>\<open>~~/src/Pure/Concurrent/synchronized.ML\<close> for details.
\<close>
text %mlex \<open>
@@ -1809,8 +1806,8 @@
text \<open>
\<^medskip>
- See @{file "~~/src/Pure/Concurrent/mailbox.ML"} how to implement a mailbox
- as synchronized variable over a purely functional list.
+ See \<^file>\<open>~~/src/Pure/Concurrent/mailbox.ML\<close> how to implement a mailbox as
+ synchronized variable over a purely functional list.
\<close>
--- a/src/Doc/Implementation/Tactic.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/Implementation/Tactic.thy Fri Aug 12 20:58:20 2016 +0200
@@ -168,9 +168,8 @@
\end{mldecls}
\<^descr> Type @{ML_type tactic} represents tactics. The well-formedness conditions
- described above need to be observed. See also @{file
- "~~/src/Pure/General/seq.ML"} for the underlying implementation of lazy
- sequences.
+ described above need to be observed. See also \<^file>\<open>~~/src/Pure/General/seq.ML\<close>
+ for the underlying implementation of lazy sequences.
\<^descr> Type @{ML_type "int -> tactic"} represents tactics with explicit subgoal
addressing, with well-formedness conditions as described above.
--- a/src/Doc/Isar_Ref/Document_Preparation.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy Fri Aug 12 20:58:20 2016 +0200
@@ -40,7 +40,7 @@
Markup commands provide a structured way to insert text into the document
generated from a theory. Each markup command takes a single @{syntax text}
argument, which is passed as argument to a corresponding {\LaTeX} macro. The
- default macros provided by @{file "~~/lib/texinputs/isabelle.sty"} can be
+ default macros provided by \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close> can be
redefined according to the needs of the underlying document and {\LaTeX}
styles.
@@ -195,8 +195,9 @@
@@{antiquotation emph} options @{syntax text} |
@@{antiquotation bold} options @{syntax text} |
@@{antiquotation verbatim} options @{syntax text} |
+ @@{antiquotation path} options @{syntax embedded} |
@@{antiquotation "file"} options @{syntax name} |
- @@{antiquotation file_unchecked} options @{syntax name} |
+ @@{antiquotation dir} options @{syntax name} |
@@{antiquotation url} options @{syntax embedded} |
@@{antiquotation cite} options @{syntax cartouche}? (@{syntax name} + @'and')
;
@@ -283,11 +284,13 @@
\<^descr> \<open>@{verbatim s}\<close> prints uninterpreted source text literally as ASCII
characters, using some type-writer font style.
- \<^descr> \<open>@{file path}\<close> checks that \<open>path\<close> refers to a file (or directory) and
- prints it verbatim.
+ \<^descr> \<open>@{path name}\<close> prints the file-system path name verbatim.
- \<^descr> \<open>@{file_unchecked path}\<close> is like \<open>@{file path}\<close>, but does not check the
- existence of the \<open>path\<close> within the file-system.
+ \<^descr> \<open>@{file name}\<close> is like \<open>@{path name}\<close>, but ensures that \<open>name\<close> refers to a
+ plain file.
+
+ \<^descr> \<open>@{dir name}\<close> is like \<open>@{path name}\<close>, but ensures that \<open>name\<close> refers to a
+ directory.
\<^descr> \<open>@{url name}\<close> produces markup for the given URL, which results in an
active hyperlink within the text.
@@ -417,8 +420,8 @@
text_raw} (\secref{sec:markup}) consist of plain text. Its internal
structure consists of paragraphs and (nested) lists, using special Isabelle
symbols and some rules for indentation and blank lines. This quasi-visual
- format resembles \<^emph>\<open>Markdown\<close>\<^footnote>\<open>@{url "http://commonmark.org"}\<close>, but the
- full complexity of that notation is avoided.
+ format resembles \<^emph>\<open>Markdown\<close>\<^footnote>\<open>\<^url>\<open>http://commonmark.org\<close>\<close>, but the full
+ complexity of that notation is avoided.
This is a summary of the main principles of minimal Markdown in Isabelle:
@@ -492,8 +495,8 @@
\<^medskip>
Command tags merely produce certain markup environments for type-setting.
- The meaning of these is determined by {\LaTeX} macros, as defined in @{file
- "~~/lib/texinputs/isabelle.sty"} or by the document author. The Isabelle
+ The meaning of these is determined by {\LaTeX} macros, as defined in
+ \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close> or by the document author. The Isabelle
document preparation tools also provide some high-level options to specify
the meaning of arbitrary tags to ``keep'', ``drop'', or ``fold'' the
corresponding parts of the text. Logic sessions may also specify ``document
@@ -514,8 +517,8 @@
\<close>}
The @{antiquotation rail} antiquotation allows to include syntax diagrams
- into Isabelle documents. {\LaTeX} requires the style file @{file
- "~~/lib/texinputs/railsetup.sty"}, which can be used via
+ into Isabelle documents. {\LaTeX} requires the style file
+ \<^file>\<open>~~/lib/texinputs/railsetup.sty\<close>, which can be used via
\<^verbatim>\<open>\usepackage{railsetup}\<close> in \<^verbatim>\<open>root.tex\<close>, for example.
The rail specification language is quoted here as Isabelle @{syntax string}
--- a/src/Doc/Isar_Ref/Framework.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/Isar_Ref/Framework.thy Fri Aug 12 20:58:20 2016 +0200
@@ -89,13 +89,13 @@
\<^medskip>
Concrete applications require another intermediate layer: an object-logic.
Isabelle/HOL @{cite "isa-tutorial"} (simply-typed set-theory) is most
- commonly used; elementary examples are given in the directory @{file
- "~~/src/HOL/Isar_Examples"}. Some examples demonstrate how to start a fresh
+ commonly used; elementary examples are given in the directory
+ \<^dir>\<open>~~/src/HOL/Isar_Examples\<close>. Some examples demonstrate how to start a fresh
object-logic from Isabelle/Pure, and use Isar proofs from the very start,
despite the lack of advanced proof tools at such an early stage (e.g.\ see
- @{file "~~/src/HOL/Isar_Examples/Higher_Order_Logic.thy"}). Isabelle/FOL
- @{cite "isabelle-logics"} and Isabelle/ZF @{cite "isabelle-ZF"} also work,
- but are much less developed.
+ \<^file>\<open>~~/src/HOL/Isar_Examples/Higher_Order_Logic.thy\<close>). Isabelle/FOL @{cite
+ "isabelle-logics"} and Isabelle/ZF @{cite "isabelle-ZF"} also work, but are
+ much less developed.
In order to illustrate natural deduction in Isar, we shall subsequently
refer to the background theory and library of Isabelle/HOL. This includes
@@ -524,7 +524,7 @@
may be populated later. The command \<^theory_text>\<open>method_setup\<close> allows to define proof
methods semantically in Isabelle/ML. The Eisbach language allows to define
proof methods symbolically, as recursive expressions over existing methods
- @{cite "Matichuk-et-al:2014"}; see also @{file "~~/src/HOL/Eisbach"}.
+ @{cite "Matichuk-et-al:2014"}; see also \<^dir>\<open>~~/src/HOL/Eisbach\<close>.
Methods use the facts indicated by \<^theory_text>\<open>then\<close> or \<^theory_text>\<open>using\<close>, and then operate on
the goal state. Some basic methods are predefined in Pure: ``@{method "-"}''
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Fri Aug 12 20:58:20 2016 +0200
@@ -538,8 +538,8 @@
\<^descr> @{method (HOL) induction_schema} derives user-specified induction rules
from well-founded induction and completeness of patterns. This factors out
some operations that are done internally by the function package and makes
- them available separately. See @{file "~~/src/HOL/ex/Induction_Schema.thy"}
- for examples.
+ them available separately. See \<^file>\<open>~~/src/HOL/ex/Induction_Schema.thy\<close> for
+ examples.
\<close>
@@ -659,8 +659,8 @@
Adhoc overloading allows to overload a constant depending on its type.
Typically this involves the introduction of an uninterpreted constant (used
for input and output) and the addition of some variants (used internally).
- For examples see @{file "~~/src/HOL/ex/Adhoc_Overloading_Examples.thy"} and
- @{file "~~/src/HOL/Library/Monad_Syntax.thy"}.
+ For examples see \<^file>\<open>~~/src/HOL/ex/Adhoc_Overloading_Examples.thy\<close> and
+ \<^file>\<open>~~/src/HOL/Library/Monad_Syntax.thy\<close>.
@{rail \<open>
(@@{command adhoc_overloading} | @@{command no_adhoc_overloading})
@@ -1013,7 +1013,7 @@
subsubsection \<open>Examples\<close>
-text \<open>See @{file "~~/src/HOL/ex/Records.thy"}, for example.\<close>
+text \<open>See \<^file>\<open>~~/src/HOL/ex/Records.thy\<close>, for example.\<close>
section \<open>Semantic subtype definitions \label{sec:hol-typedef}\<close>
@@ -1411,28 +1411,26 @@
\<^descr> @{attribute (HOL) quot_map} registers a quotient map theorem, a theorem
showing how to ``lift'' quotients over type constructors. E.g.\ @{term
"Quotient R Abs Rep T \<Longrightarrow> Quotient (rel_set R) (image Abs) (image Rep)
- (rel_set T)"}. For examples see @{file "~~/src/HOL/Lifting_Set.thy"} or
- @{file "~~/src/HOL/Lifting.thy"}. This property is proved automatically if
- the involved type is BNF without dead variables.
+ (rel_set T)"}. For examples see \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or
+ \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property is proved automatically if the
+ involved type is BNF without dead variables.
\<^descr> @{attribute (HOL) relator_eq_onp} registers a theorem that shows that a
relator applied to an equality restricted by a predicate @{term P} (i.e.\
@{term "eq_onp P"}) is equal to a predicator applied to the @{term P}. The
combinator @{const eq_onp} is used for internal encoding of proper subtypes.
Such theorems allows the package to hide \<open>eq_onp\<close> from a user in a
- user-readable form of a respectfulness theorem. For examples see @{file
- "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. This
- property is proved automatically if the involved type is BNF without dead
- variables.
+ user-readable form of a respectfulness theorem. For examples see
+ \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property
+ is proved automatically if the involved type is BNF without dead variables.
\<^descr> @{attribute (HOL) "relator_mono"} registers a property describing a
monotonicity of a relator. E.g.\ @{prop "A \<le> B \<Longrightarrow> rel_set A \<le> rel_set B"}.
This property is needed for proving a stronger transfer rule in
@{command_def (HOL) "lift_definition"} when a parametricity theorem for the
raw term is specified and also for the reflexivity prover. For examples see
- @{file "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
- This property is proved automatically if the involved type is BNF without
- dead variables.
+ \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property
+ is proved automatically if the involved type is BNF without dead variables.
\<^descr> @{attribute (HOL) "relator_distr"} registers a property describing a
distributivity of the relation composition and a relator. E.g.\ \<open>rel_set R
@@ -1443,9 +1441,9 @@
specified each direction separately and also register multiple theorems with
different set of assumptions. This attribute can be used only after the
monotonicity property was already registered by @{attribute (HOL)
- "relator_mono"}. For examples see @{file "~~/src/HOL/Lifting_Set.thy"} or
- @{file "~~/src/HOL/Lifting.thy"}. This property is proved automatically if
- the involved type is BNF without dead variables.
+ "relator_mono"}. For examples see \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or
+ \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property is proved automatically if the
+ involved type is BNF without dead variables.
\<^descr> @{attribute (HOL) quot_del} deletes a corresponding Quotient theorem from
the Lifting infrastructure and thus de-register the corresponding quotient.
@@ -1524,7 +1522,7 @@
"transfer_step"}+, @{method (HOL) "transfer_end"}) and @{method (HOL)
"transfer_prover"} = (@{method (HOL) "transfer_prover_start"}, @{method
(HOL) "transfer_step"}+, @{method (HOL) "transfer_prover_end"}). For usage
- examples see @{file "~~/src/HOL/ex/Transfer_Debug.thy"}
+ examples see \<^file>\<open>~~/src/HOL/ex/Transfer_Debug.thy\<close>.
\<^descr> @{attribute (HOL) "untransferred"} proves the same equivalent theorem as
@{method (HOL) "transfer"} internally does.
@@ -1566,17 +1564,15 @@
relators of various type constructors, e.g. @{term "rel_set (op =) = (op
=)"}. The @{method (HOL) transfer} method uses these lemmas to infer
transfer rules for non-polymorphic constants on the fly. For examples see
- @{file "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}.
- This property is proved automatically if the involved type is BNF without
- dead variables.
+ \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property
+ is proved automatically if the involved type is BNF without dead variables.
\<^descr> @{attribute_def (HOL) "relator_domain"} attribute collects rules
describing domains of relators by predicators. E.g.\ @{term "Domainp
(rel_set T) = (\<lambda>A. Ball A (Domainp T))"}. This allows the package to lift
- transfer domain rules through type constructors. For examples see @{file
- "~~/src/HOL/Lifting_Set.thy"} or @{file "~~/src/HOL/Lifting.thy"}. This
- property is proved automatically if the involved type is BNF without dead
- variables.
+ transfer domain rules through type constructors. For examples see
+ \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property
+ is proved automatically if the involved type is BNF without dead variables.
Theoretical background can be found in @{cite
@@ -2082,14 +2078,13 @@
\<close>}
\<^descr> @{method (HOL) meson} implements Loveland's model elimination procedure
- @{cite "loveland-78"}. See @{file "~~/src/HOL/ex/Meson_Test.thy"} for
- examples.
+ @{cite "loveland-78"}. See \<^file>\<open>~~/src/HOL/ex/Meson_Test.thy\<close> for examples.
\<^descr> @{method (HOL) metis} combines ordered resolution and ordered
paramodulation to find first-order (or mildly higher-order) proofs. The
first optional argument specifies a type encoding; see the Sledgehammer
- manual @{cite "isabelle-sledgehammer"} for details. The directory @{file
- "~~/src/HOL/Metis_Examples"} contains several small theories developed to a
+ manual @{cite "isabelle-sledgehammer"} for details. The directory
+ \<^dir>\<open>~~/src/HOL/Metis_Examples\<close> contains several small theories developed to a
large extent using @{method (HOL) metis}.
\<close>
@@ -2168,7 +2163,7 @@
(*<*)end(*>*)
text \<open>
- See also @{file "~~/src/HOL/ex/Groebner_Examples.thy"}.
+ See also \<^file>\<open>~~/src/HOL/ex/Groebner_Examples.thy\<close>.
\<close>
@@ -2185,8 +2180,8 @@
\<^descr> @{method (HOL) coherent} solves problems of \<^emph>\<open>Coherent Logic\<close> @{cite
"Bezem-Coquand:2005"}, which covers applications in confluence theory,
- lattice theory and projective geometry. See @{file
- "~~/src/HOL/ex/Coherent.thy"} for some examples.
+ lattice theory and projective geometry. See \<^file>\<open>~~/src/HOL/ex/Coherent.thy\<close>
+ for some examples.
\<close>
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Fri Aug 12 20:58:20 2016 +0200
@@ -571,8 +571,8 @@
float_token}, @{syntax (inner) str_token}, @{syntax (inner) string_token},
and @{syntax (inner) cartouche} are not used in Pure. Object-logics may
implement numerals and string literals by adding appropriate syntax
- declarations, together with some translation functions (e.g.\ see @{file
- "~~/src/HOL/Tools/string_syntax.ML"}).
+ declarations, together with some translation functions (e.g.\ see
+ \<^file>\<open>~~/src/HOL/Tools/string_syntax.ML\<close>).
The derived categories @{syntax_def (inner) num_const}, and @{syntax_def
(inner) float_const}, provide robust access to the respective tokens: the
--- a/src/Doc/Isar_Ref/Spec.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Fri Aug 12 20:58:20 2016 +0200
@@ -1303,8 +1303,8 @@
the scope of the resulting theory.
- See @{file "~~/src/HOL/ex/Iff_Oracle.thy"} for a worked example of defining
- a new primitive rule as oracle, and turning it into a proof method.
+ See \<^file>\<open>~~/src/HOL/ex/Iff_Oracle.thy\<close> for a worked example of defining a new
+ primitive rule as oracle, and turning it into a proof method.
\<close>
--- a/src/Doc/Isar_Ref/Synopsis.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/Isar_Ref/Synopsis.thy Fri Aug 12 20:58:20 2016 +0200
@@ -214,7 +214,7 @@
section \<open>Calculational reasoning \label{sec:calculations-synopsis}\<close>
text \<open>
- For example, see @{file "~~/src/HOL/Isar_Examples/Group.thy"}.
+ For example, see \<^file>\<open>~~/src/HOL/Isar_Examples/Group.thy\<close>.
\<close>
--- a/src/Doc/Isar_Ref/document/showsymbols Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/Isar_Ref/document/showsymbols Fri Aug 12 20:58:20 2016 +0200
@@ -5,11 +5,13 @@
$eol = "&";
while (<ARGV>) {
- if (m/^\\newcommand\{\\isasym([A-Za-z]+)\}/) {
- print "\\verb,\\<$1>, & {\\isasym$1} $eol\n";
-# print "\\verb,\\<$1>, & \\isactrlbold{\\isasym$1}~{\\isasym$1} $eol\n";
-# print "\\verb,\\<$1>, & B\\isactrlsup{\\isasym$1} $eol\n";
-# print "\\verb,\\<$1>, & B\\isactrlsub{\\isasym$1} $eol\n";
+ if (m/^\\newcommand\{\\(isasym|isactrl)([A-Za-z]+)\}/) {
+ if ($1 eq "isasym") {
+ print "\\verb,\\<$2>, & {\\isasym$2} $eol\n";
+ }
+ else {
+ print "\\verb,\\<^$2>, & {\\isactrl$2} $eol\n";
+ }
if ("$eol" eq "&") {
$eol = "\\\\";
} else {
--- a/src/Doc/JEdit/JEdit.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/JEdit/JEdit.thy Fri Aug 12 20:58:20 2016 +0200
@@ -37,11 +37,10 @@
given up; instead there is direct support for editing of source text, with
rich formal markup for GUI rendering.
- \<^descr>[jEdit] is a sophisticated text editor\<^footnote>\<open>@{url "http://www.jedit.org"}\<close>
- implemented in Java\<^footnote>\<open>@{url "http://www.java.com"}\<close>. It is easily
- extensible by plugins written in any language that works on the JVM. In
- the context of Isabelle this is always Scala\<^footnote>\<open>@{url
- "http://www.scala-lang.org"}\<close>.
+ \<^descr>[jEdit] is a sophisticated text editor\<^footnote>\<open>\<^url>\<open>http://www.jedit.org\<close>\<close>
+ implemented in Java\<^footnote>\<open>\<^url>\<open>http://www.java.com\<close>\<close>. It is easily extensible by
+ plugins written in any language that works on the JVM. In the context of
+ Isabelle this is always Scala\<^footnote>\<open>\<^url>\<open>http://www.scala-lang.org\<close>\<close>.
\<^descr>[Isabelle/jEdit] is the main application of the PIDE framework and the
default user-interface for Isabelle. It targets both beginners and
@@ -166,12 +165,12 @@
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
- @{file_unchecked "$ISABELLE_HOME_USER/jedit/properties"} and
- @{file_unchecked "$ISABELLE_HOME_USER/jedit/keymaps"}.
+ two within the central options dialog. Changes are stored in @{path
+ "$ISABELLE_HOME_USER/jedit/properties"} and @{path
+ "$ISABELLE_HOME_USER/jedit/keymaps"}.
Isabelle system options are managed by Isabelle/Scala and changes are stored
- in @{file_unchecked "$ISABELLE_HOME_USER/etc/preferences"}, independently of
+ in @{path "$ISABELLE_HOME_USER/etc/preferences"}, independently of
other jEdit properties. See also @{cite "isabelle-system"}, especially the
coverage of sessions and command-line tools like @{tool build} or @{tool
options}.
@@ -193,8 +192,8 @@
\<^medskip>
Options are usually loaded on startup and saved on shutdown of
- Isabelle/jEdit. Editing the machine-generated @{file_unchecked
- "$ISABELLE_HOME_USER/jedit/properties"} or @{file_unchecked
+ Isabelle/jEdit. Editing the machine-generated @{path
+ "$ISABELLE_HOME_USER/jedit/properties"} or @{path
"$ISABELLE_HOME_USER/etc/preferences"} manually while the application is
running is likely to cause surprise due to lost update!
\<close>
@@ -213,9 +212,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 @{file_unchecked "$ISABELLE_HOME_USER/jedit/keymaps"} versus
- \<^verbatim>\<open>shortcut\<close> properties in @{file
- "$ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props"}).
+ (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>).
\<close>
@@ -272,8 +270,8 @@
The \<^verbatim>\<open>-b\<close> and \<^verbatim>\<open>-f\<close> options control the self-build mechanism of
Isabelle/jEdit. This is only relevant for building from sources, which also
- requires an auxiliary \<^verbatim>\<open>jedit_build\<close> component from @{url
- "http://isabelle.in.tum.de/components"}. The official Isabelle release
+ requires an auxiliary \<^verbatim>\<open>jedit_build\<close> component from
+ \<^url>\<open>http://isabelle.in.tum.de/components\<close>. The official Isabelle release
already includes a pre-built version of Isabelle/jEdit.
\<^bigskip>
@@ -469,8 +467,8 @@
``\<^verbatim>\<open>\<alpha>\<close>''. For the editor front-end, a certain subset of symbols is rendered
physically via Unicode glyphs, in order to show ``\<^verbatim>\<open>\<alpha>\<close>'' as ``\<open>\<alpha>\<close>'', for
example. This symbol interpretation is specified by the Isabelle system
- distribution in @{file "$ISABELLE_HOME/etc/symbols"} and may be augmented by
- the user in @{file_unchecked "$ISABELLE_HOME_USER/etc/symbols"}.
+ distribution in \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> and may be augmented by the
+ user in @{path "$ISABELLE_HOME_USER/etc/symbols"}.
The appendix of @{cite "isabelle-isar-ref"} gives an overview of the
standard interpretation of finitely many symbols from the infinite
@@ -551,7 +549,7 @@
\<^verbatim>\<open>\lambda\<close>, or its ASCII abbreviation \<^verbatim>\<open>%\<close> by the Unicode rendering.
The following table is an extract of the information provided by the
- standard @{file "$ISABELLE_HOME/etc/symbols"} file:
+ standard \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> file:
\<^medskip>
\begin{tabular}{lll}
@@ -660,9 +658,8 @@
platforms. Isabelle/ML on Windows uses Unix-style path notation, too, and
driver letter representation as in Cygwin (e.g.\ \<^verbatim>\<open>/cygdrive/c\<close>). Moreover,
environment variables from the Isabelle process may be used freely, e.g.\
- @{file "$ISABELLE_HOME/etc/symbols"} or @{file_unchecked
- "$POLYML_HOME/README"}. There are special shortcuts: @{file "~"} for @{file
- "$USER_HOME"} and @{file "~~"} for @{file "$ISABELLE_HOME"}.
+ \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> or \<^file>\<open>$POLYML_HOME/README\<close>. There are special
+ shortcuts: \<^dir>\<open>~\<close> for \<^dir>\<open>$USER_HOME\<close> and \<^dir>\<open>~~\<close> for \<^dir>\<open>$ISABELLE_HOME\<close>.
\<^medskip>
Since jEdit happens to support environment variables within file
@@ -849,8 +846,8 @@
further tricks to manage markup of ML files, such that Isabelle/HOL may be
edited conveniently in the Prover IDE on small machines with only 8\,GB of
main memory. Using \<^verbatim>\<open>Pure\<close> as logic session image, the exploration may start
- at the top @{file "$ISABELLE_HOME/src/HOL/Main.thy"} or the bottom @{file
- "$ISABELLE_HOME/src/HOL/HOL.thy"}, for example.
+ at the top \<^file>\<open>$ISABELLE_HOME/src/HOL/Main.thy\<close> or the bottom
+ \<^file>\<open>$ISABELLE_HOME/src/HOL/HOL.thy\<close>, for example.
Initially, before an auxiliary file is opened in the editor, the prover
reads its content from the physical file-system. After the file is opened
@@ -875,8 +872,8 @@
Warnings, errors, and other useful markup is attached directly to the
positions in the auxiliary file buffer, in the manner of standard IDEs. By
- using the load command @{command SML_file} as explained in @{file
- "$ISABELLE_HOME/src/Tools/SML/Examples.thy"}, Isabelle/jEdit may be used as
+ using the load command @{command SML_file} as explained in
+ \<^file>\<open>$ISABELLE_HOME/src/Tools/SML/Examples.thy\<close>, Isabelle/jEdit may be used as
fully-featured IDE for Standard ML, independently of theory or proof
development: the required theory merely serves as some kind of project file
for a collection of SML source modules.
@@ -1045,8 +1042,7 @@
\<^item> The \<^emph>\<open>Search\<close> field allows to highlight query output according to some
regular expression, in the notation that is commonly used on the Java
- platform.\<^footnote>\<open>@{url
- "https://docs.oracle.com/javase/8/docs/api/java/util/regex/Pattern.html"}\<close>
+ platform.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/javase/8/docs/api/java/util/regex/Pattern.html\<close>\<close>
This may serve as an additional visual filter of the result.
\<^item> The \<^emph>\<open>Zoom\<close> box controls the font size of the output area.
@@ -1241,9 +1237,8 @@
text \<open>
The completion tables for Isabelle symbols (\secref{sec:symbols}) are
- determined statically from @{file "$ISABELLE_HOME/etc/symbols"} and
- @{file_unchecked "$ISABELLE_HOME_USER/etc/symbols"} for each symbol
- specification as follows:
+ determined statically from \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> and @{path
+ "$ISABELLE_HOME_USER/etc/symbols"} for each symbol specification as follows:
\<^medskip>
\begin{tabular}{ll}
@@ -1273,13 +1268,12 @@
which do not allow arbitrary backslash sequences.
\<^medskip>
- Additional abbreviations may be specified in @{file
- "$ISABELLE_HOME/etc/abbrevs"} and @{file_unchecked
- "$ISABELLE_HOME_USER/etc/abbrevs"}. The file content follows general Isar
- outer syntax @{cite "isabelle-isar-ref"}. Abbreviations are specified as
- ``\<open>abbrev\<close>~\<^verbatim>\<open>=\<close>~\<open>text\<close>'' pairs. The replacement \<open>text\<close> may consist of more
- than just one symbol; otherwise the meaning is the same as a symbol
- specification ``\<open>sym\<close>~\<^verbatim>\<open>abbrev:\<close>~\<open>abbrev\<close>'' within @{file_unchecked
+ Additional abbreviations may be specified in \<^file>\<open>$ISABELLE_HOME/etc/abbrevs\<close>
+ and @{path "$ISABELLE_HOME_USER/etc/abbrevs"}. The file content follows
+ general Isar outer syntax @{cite "isabelle-isar-ref"}. Abbreviations are
+ specified as ``\<open>abbrev\<close>~\<^verbatim>\<open>=\<close>~\<open>text\<close>'' pairs. The replacement \<open>text\<close> may
+ consist of more than just one symbol; otherwise the meaning is the same as a
+ symbol specification ``\<open>sym\<close>~\<^verbatim>\<open>abbrev:\<close>~\<open>abbrev\<close>'' within @{path
"etc/symbols"}.
\<close>
@@ -1544,7 +1538,7 @@
dictionary, taken from the colon-separated list in the settings variable
@{setting_def JORTHO_DICTIONARIES}. There are jEdit actions to specify local
updates to a dictionary, by including or excluding words. The result of
- permanent dictionary updates is stored in the directory @{file_unchecked
+ permanent dictionary updates is stored in the directory @{path
"$ISABELLE_HOME_USER/dictionaries"}, in a separate file for each dictionary.
\<^item> @{system_option_def spell_checker_elements} specifies a comma-separated
@@ -1719,10 +1713,10 @@
text \<open>
Document text is internally structured in paragraphs and nested lists, using
- notation that is similar to Markdown\<^footnote>\<open>@{url "http://commonmark.org"}\<close>. There
- are special control symbols for items of different kinds of lists,
- corresponding to \<^verbatim>\<open>itemize\<close>, \<^verbatim>\<open>enumerate\<close>, \<^verbatim>\<open>description\<close> in {\LaTeX}. This
- is illustrated in for \<^verbatim>\<open>itemize\<close> in \figref{fig:markdown-document}.
+ notation that is similar to Markdown\<^footnote>\<open>\<^url>\<open>http://commonmark.org\<close>\<close>. There are
+ special control symbols for items of different kinds of lists, corresponding
+ to \<^verbatim>\<open>itemize\<close>, \<^verbatim>\<open>enumerate\<close>, \<^verbatim>\<open>description\<close> in {\LaTeX}. This is illustrated
+ in for \<^verbatim>\<open>itemize\<close> in \figref{fig:markdown-document}.
\begin{figure}[!htb]
\begin{center}
@@ -1782,7 +1776,7 @@
chapter \<open>ML debugging within the Prover IDE\<close>
text \<open>
- Isabelle/ML is based on Poly/ML\<^footnote>\<open>@{url "http://www.polyml.org"}\<close> and thus
+ Isabelle/ML is based on Poly/ML\<^footnote>\<open>\<^url>\<open>http://www.polyml.org\<close>\<close> and thus
benefits from the source-level debugger of that implementation of Standard
ML. The Prover IDE provides the \<^emph>\<open>Debugger\<close> dockable to connect to running
ML threads, inspect the stack frame with local ML bindings, and evaluate ML
@@ -2003,7 +1997,7 @@
\<^bold>\<open>Workaround:\<close> Install \<^verbatim>\<open>IsabelleText\<close> and \<^verbatim>\<open>IsabelleTextBold\<close> on the system
with \<^emph>\<open>Font Book\<close>, despite the warnings in \secref{sec:symbols} against
- that! The \<^verbatim>\<open>.ttf\<close> font files reside in some directory @{file_unchecked
+ that! The \<^verbatim>\<open>.ttf\<close> font files reside in some directory @{path
"$ISABELLE_HOME/contrib/isabelle_fonts-XYZ"}.
\<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus tend to disrupt key
--- a/src/Doc/Locales/Examples3.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/Locales/Examples3.thy Fri Aug 12 20:58:20 2016 +0200
@@ -525,7 +525,7 @@
The sources of this tutorial, which include all proofs, are
available with the Isabelle distribution at
- @{url "http://isabelle.in.tum.de"}.
+ \<^url>\<open>http://isabelle.in.tum.de\<close>.
\<close>
text \<open>
--- a/src/Doc/Main/Main_Doc.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/Main/Main_Doc.thy Fri Aug 12 20:58:20 2016 +0200
@@ -26,7 +26,7 @@
text\<open>
\begin{abstract}
-This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. For infix operators and their precedences see the final section. The sophisticated class structure is only hinted at. For details see @{url "http://isabelle.in.tum.de/library/HOL/"}.
+This document lists the main types, functions and syntax provided by theory @{theory Main}. It is meant as a quick overview of what is available. For infix operators and their precedences see the final section. The sophisticated class structure is only hinted at. For details see \<^url>\<open>http://isabelle.in.tum.de/library/HOL\<close>.
\end{abstract}
\section*{HOL}
--- a/src/Doc/Prog_Prove/Basics.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/Prog_Prove/Basics.thy Fri Aug 12 20:58:20 2016 +0200
@@ -124,9 +124,9 @@
\end{warn}
In addition to the theories that come with the Isabelle/HOL distribution
-(see @{url "http://isabelle.in.tum.de/library/HOL/"})
+(see \<^url>\<open>http://isabelle.in.tum.de/library/HOL\<close>)
there is also the \emph{Archive of Formal Proofs}
-at @{url "http://afp.sourceforge.net"}, a growing collection of Isabelle theories
+at \<^url>\<open>http://afp.sourceforge.net\<close>, a growing collection of Isabelle theories
that everybody can contribute to.
\subsection{Quotation Marks}
--- a/src/Doc/System/Environment.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/System/Environment.thy Fri Aug 12 20:58:20 2016 +0200
@@ -44,11 +44,10 @@
that the Isabelle executables either have to be run from their original
location in the distribution directory, or via the executable objects
created by the @{tool install} tool. Symbolic links are admissible, but a
- plain copy of the @{file "$ISABELLE_HOME/bin"} files will not work!
+ plain copy of the \<^dir>\<open>$ISABELLE_HOME/bin\<close> files will not work!
- \<^enum> The file @{file "$ISABELLE_HOME/etc/settings"} is run as a
- @{executable_ref bash} shell script with the auto-export option for
- variables enabled.
+ \<^enum> The file \<^file>\<open>$ISABELLE_HOME/etc/settings\<close> is run as a @{executable_ref
+ bash} shell script with the auto-export option for variables enabled.
This file holds a rather long list of shell variable assignments, thus
providing the site-wide default settings. The Isabelle distribution
@@ -56,15 +55,15 @@
variables. When installing the system, only a few of these may have to be
adapted (probably @{setting ML_SYSTEM} etc.).
- \<^enum> The file @{file_unchecked "$ISABELLE_HOME_USER/etc/settings"} (if it
+ \<^enum> The file @{path "$ISABELLE_HOME_USER/etc/settings"} (if it
exists) is run in the same way as the site default settings. Note that the
variable @{setting ISABELLE_HOME_USER} has already been set before ---
usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/IsabelleXXXX\<close>.
Thus individual users may override the site-wide defaults. Typically, a
user settings file contains only a few lines, with some assignments that
- are actually changed. Never copy the central @{file
- "$ISABELLE_HOME/etc/settings"} file!
+ are actually changed. Never copy the central
+ \<^file>\<open>$ISABELLE_HOME/etc/settings\<close> file!
Since settings files are regular GNU @{executable_def bash} scripts, one may
use complex shell commands, such as \<^verbatim>\<open>if\<close> or \<^verbatim>\<open>case\<close> statements to set
@@ -101,8 +100,8 @@
On Unix systems this is usually the same as @{setting HOME}, but on Windows
it is the regular home directory of the user, not the one of within the
Cygwin root file-system.\<^footnote>\<open>Cygwin itself offers another choice whether its
- HOME should point to the @{file_unchecked "/home"} directory tree or the
- Windows user home.\<close>
+ HOME should point to the @{path "/home"} directory tree or the Windows user
+ home.\<close>
\<^descr>[@{setting_def ISABELLE_HOME}\<open>\<^sup>*\<close>] is the location of the top-level
Isabelle distribution directory. This is automatically determined from the
@@ -110,7 +109,7 @@
ISABELLE_HOME} yourself from the shell!
\<^descr>[@{setting_def ISABELLE_HOME_USER}] is the user-specific counterpart of
- @{setting ISABELLE_HOME}. The default value is relative to @{file_unchecked
+ @{setting ISABELLE_HOME}. The default value is relative to @{path
"$USER_HOME/.isabelle"}, under rare circumstances this may be changed in the
global setting file. Typically, the @{setting ISABELLE_HOME_USER} directory
mimics @{setting ISABELLE_HOME} to some extend. In particular, site-wide
@@ -138,7 +137,7 @@
\<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name
of the @{executable isabelle} executable. Thus other tools and scripts need
- not assume that the @{file "$ISABELLE_HOME/bin"} directory is on the current
+ not assume that the \<^dir>\<open>$ISABELLE_HOME/bin\<close> directory is on the current
search path of the shell.
\<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this
@@ -147,8 +146,8 @@
\<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def
ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>]
specify the underlying ML system to be used for Isabelle. There is only a
- fixed set of admissable @{setting ML_SYSTEM} names (see the @{file
- "$ISABELLE_HOME/etc/settings"} file of the distribution).
+ fixed set of admissable @{setting ML_SYSTEM} names (see the
+ \<^file>\<open>$ISABELLE_HOME/etc/settings\<close> file of the distribution).
The actual compiler binary will be run from the directory @{setting
ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the command line.
@@ -175,7 +174,7 @@
\<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where theory
browser information is stored as HTML and PDF (see also \secref{sec:info}).
- The default value is @{file_unchecked "$ISABELLE_HOME_USER/browser_info"}.
+ The default value is @{path "$ISABELLE_HOME_USER/browser_info"}.
\<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none
is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>.
@@ -234,12 +233,12 @@
The root of component initialization is @{setting ISABELLE_HOME} itself.
After initializing all of its sub-components recursively, @{setting
ISABELLE_HOME_USER} is included in the same manner (if that directory
- exists). This allows to install private components via @{file_unchecked
+ exists). This allows to install private components via @{path
"$ISABELLE_HOME_USER/etc/components"}, although it is often more convenient
to do that programmatically via the \<^verbatim>\<open>init_component\<close> shell function in the
\<^verbatim>\<open>etc/settings\<close> script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component
- directory). For example:
- @{verbatim [display] \<open>init_component "$HOME/screwdriver-2.0"\<close>}
+ directory). For example: @{verbatim [display] \<open>init_component
+ "$HOME/screwdriver-2.0"\<close>}
This is tolerant wrt.\ missing component directories, but might produce a
warning.
@@ -429,8 +428,8 @@
separated by \<open>\<^bold>X\<close>, then split each chunk into sub-chunks separated by \<open>\<^bold>Y\<close>.
Markup chunks start with an empty sub-chunk, and a second empty sub-chunk
indicates close of an element. Any other non-empty chunk consists of plain
- text. For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or @{file
- "~~/src/Pure/PIDE/yxml.scala"}.
+ text. For example, see \<^file>\<open>~~/src/Pure/PIDE/yxml.ML\<close> or
+ \<^file>\<open>~~/src/Pure/PIDE/yxml.scala\<close>.
YXML documents may be detected quickly by checking that the first two
characters are \<open>\<^bold>X\<^bold>Y\<close>.
--- a/src/Doc/System/Misc.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/System/Misc.thy Fri Aug 12 20:58:20 2016 +0200
@@ -34,8 +34,8 @@
Components are initialized as described in \secref{sec:components} in a
permissive manner, which can mark components as ``missing''. This state is
amended by letting @{tool "components"} download and unpack components that
- are published on the default component repository @{url
- "http://isabelle.in.tum.de/components/"} in particular.
+ are published on the default component repository
+ \<^url>\<open>http://isabelle.in.tum.de/components\<close> in particular.
Option \<^verbatim>\<open>-R\<close> specifies an alternative component repository. Note that
\<^verbatim>\<open>file:///\<close> URLs can be used for local directories.
--- a/src/Doc/System/Presentation.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/System/Presentation.thy Fri Aug 12 20:58:20 2016 +0200
@@ -69,9 +69,9 @@
The presentation output will appear in \<^verbatim>\<open>$ISABELLE_BROWSER_INFO/FOL/FOL\<close> as
reported by the above verbose invocation of the build process.
- Many Isabelle sessions (such as \<^verbatim>\<open>HOL-Library\<close> in @{file
- "~~/src/HOL/Library"}) also provide printable documents in PDF. These are
- prepared automatically as well if enabled like this:
+ Many Isabelle sessions (such as \<^verbatim>\<open>HOL-Library\<close> in \<^dir>\<open>~~/src/HOL/Library\<close>)
+ also provide printable documents in PDF. These are prepared automatically as
+ well if enabled like this:
@{verbatim [display] \<open>isabelle build -o browser_info -o document=pdf -v -c HOL-Library\<close>}
Enabling both browser info and document preparation simultaneously causes an
@@ -177,8 +177,8 @@
drop, and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to fold text tagged as \<open>foo\<close>. The builtin default is
equivalent to the tag specification
``\<^verbatim>\<open>+theory,+proof,+ML,+visible,-invisible\<close>''; see also the {\LaTeX} macros
- \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and \<^verbatim>\<open>\isafoldtag\<close>, in @{file
- "~~/lib/texinputs/isabelle.sty"}.
+ \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and \<^verbatim>\<open>\isafoldtag\<close>, in
+ \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>.
\<^medskip>
Document preparation requires a \<^verbatim>\<open>document\<close> directory within the session
@@ -211,8 +211,8 @@
user would include \<^verbatim>\<open>session.tex\<close> to get a document containing all the
theories.
- The {\LaTeX} versions of the theories require some macros defined in @{file
- "~~/lib/texinputs/isabelle.sty"}. Doing \<^verbatim>\<open>\usepackage{isabelle}\<close> in
+ The {\LaTeX} versions of the theories require some macros defined in
+ \<^file>\<open>~~/lib/texinputs/isabelle.sty\<close>. Doing \<^verbatim>\<open>\usepackage{isabelle}\<close> in
\<^verbatim>\<open>root.tex\<close> should be fine; the underlying @{tool latex} already includes an
appropriate path specification for {\TeX} inputs.
@@ -221,11 +221,11 @@
standard set of {\LaTeX} macro definitions \<^verbatim>\<open>\isasym\<close>\<open>foo\<close> corresponding to
\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>foo\<close>\<^verbatim>\<open>>\<close>, see @{cite "isabelle-implementation"} for a complete list
of predefined Isabelle symbols. Users may invent further symbols as well,
- just by providing {\LaTeX} macros in a similar fashion as in @{file
- "~~/lib/texinputs/isabellesym.sty"} of the Isabelle distribution.
+ just by providing {\LaTeX} macros in a similar fashion as in
+ \<^file>\<open>~~/lib/texinputs/isabellesym.sty\<close> of the Isabelle distribution.
For proper setup of DVI and PDF documents (with hyperlinks and bookmarks),
- we recommend to include @{file "~~/lib/texinputs/pdfsetup.sty"} as well.
+ we recommend to include \<^file>\<open>~~/lib/texinputs/pdfsetup.sty\<close> as well.
\<^medskip>
As a final step of Isabelle document preparation, @{tool document}~\<^verbatim>\<open>-c\<close> is
--- a/src/Doc/System/Scala.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/System/Scala.thy Fri Aug 12 20:58:20 2016 +0200
@@ -88,8 +88,8 @@
This assumes that the executable may be found via the @{setting PATH} from
the process environment: this is the case when Isabelle settings are active,
e.g.\ in the context of the main Isabelle tool wrapper
- \secref{sec:isabelle-tool}. Alternatively, the full @{file
- "$ISABELLE_HOME/bin/isabelle_scala_script"} may be specified in expanded
+ \secref{sec:isabelle-tool}. Alternatively, the full
+ \<^file>\<open>$ISABELLE_HOME/bin/isabelle_scala_script\<close> may be specified in expanded
form.
\<close>
--- a/src/Doc/System/Sessions.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Doc/System/Sessions.thy Fri Aug 12 20:58:20 2016 +0200
@@ -140,19 +140,18 @@
subsubsection \<open>Examples\<close>
text \<open>
- See @{file "~~/src/HOL/ROOT"} for a diversity of practically relevant
- situations, although it uses relatively complex quasi-hierarchic naming
- conventions like \<^verbatim>\<open>HOL-SPARK\<close>, \<^verbatim>\<open>HOL-SPARK-Examples\<close>. An alternative is to
- use unqualified names that are relatively long and descriptive, as in the
- Archive of Formal Proofs (@{url "http://afp.sourceforge.net"}), for
- example.
+ See \<^file>\<open>~~/src/HOL/ROOT\<close> for a diversity of practically relevant situations,
+ although it uses relatively complex quasi-hierarchic naming conventions like
+ \<^verbatim>\<open>HOL-SPARK\<close>, \<^verbatim>\<open>HOL-SPARK-Examples\<close>. An alternative is to use unqualified
+ names that are relatively long and descriptive, as in the Archive of Formal
+ Proofs (\<^url>\<open>http://afp.sourceforge.net\<close>), for example.
\<close>
section \<open>System build options \label{sec:system-options}\<close>
text \<open>
- See @{file "~~/etc/options"} for the main defaults provided by the Isabelle
+ See \<^file>\<open>~~/etc/options\<close> for the main defaults provided by the Isabelle
distribution. Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple
editing mode \<^verbatim>\<open>isabelle-options\<close> for this file-format.
@@ -344,9 +343,9 @@
\<^medskip>
Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close>, which means that resulting heap images
- and log files are stored in @{file_unchecked "$ISABELLE_HOME/heaps"} instead
- of the default location @{setting ISABELLE_OUTPUT} (which is normally in
- @{setting ISABELLE_HOME_USER}, i.e.\ the user's home directory).
+ and log files are stored in @{path "$ISABELLE_HOME/heaps"} instead of the
+ default location @{setting ISABELLE_OUTPUT} (which is normally in @{setting
+ ISABELLE_HOME_USER}, i.e.\ the user's home directory).
\<^medskip>
Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity. Option \<^verbatim>\<open>-l\<close> lists
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Aug 12 20:58:20 2016 +0200
@@ -9152,8 +9152,8 @@
subsection \<open>Geometric progression\<close>
-text \<open>FIXME: Should one or more of these theorems be moved to @{file
-"~~/src/HOL/Set_Interval.thy"}, alongside \<open>geometric_sum\<close>?\<close>
+text \<open>FIXME: Should one or more of these theorems be moved to
+ \<^file>\<open>~~/src/HOL/Set_Interval.thy\<close>, alongside \<open>geometric_sum\<close>?\<close>
lemma sum_gp_basic:
fixes x :: "'a::ring_1"
--- a/src/HOL/Analysis/Linear_Algebra.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Fri Aug 12 20:58:20 2016 +0200
@@ -1654,8 +1654,8 @@
qed
text \<open>TODO: The following lemmas about adjoints should hold for any
-Hilbert space (i.e. complete inner product space).
-(see @{url "http://en.wikipedia.org/wiki/Hermitian_adjoint"})
+ Hilbert space (i.e. complete inner product space).
+ (see \<^url>\<open>http://en.wikipedia.org/wiki/Hermitian_adjoint\<close>)
\<close>
lemma adjoint_works:
--- a/src/HOL/Bali/Decl.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Bali/Decl.thy Fri Aug 12 20:58:20 2016 +0200
@@ -15,7 +15,7 @@
\item clarification and correction of some aspects of the package/access concept
(Also submitted as bug report to the Java Bug Database:
Bug Id: 4485402 and Bug Id: 4493343
- @{url "http://developer.java.sun.com/developer/bugParade/index.jshtml"}
+ \<^url>\<open>http://developer.java.sun.com/developer/bugParade/index.jshtml\<close>
)
\end{itemize}
simplifications:
--- a/src/HOL/Binomial.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Binomial.thy Fri Aug 12 20:58:20 2016 +0200
@@ -502,7 +502,7 @@
subsection \<open>Pochhammer's symbol: generalized rising factorial\<close>
-text \<open>See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"}\<close>
+text \<open>See \<^url>\<open>http://en.wikipedia.org/wiki/Pochhammer_symbol\<close>.\<close>
context comm_semiring_1
begin
--- a/src/HOL/Groups.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Groups.thy Fri Aug 12 20:58:20 2016 +0200
@@ -602,7 +602,7 @@
\<^item> \<^emph>\<open>Partially Ordered Algebraic Systems\<close>, Pergamon Press, 1963
Most of the used notions can also be looked up in
- \<^item> @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
+ \<^item> \<^url>\<open>http://www.mathworld.com\<close> by Eric Weisstein et. al.
\<^item> \<^emph>\<open>Algebra I\<close> by van der Waerden, Springer
\<close>
--- a/src/HOL/HOLCF/IOA/RefCorrectness.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/HOLCF/IOA/RefCorrectness.thy Fri Aug 12 20:58:20 2016 +0200
@@ -32,7 +32,7 @@
Axioms for fair trace inclusion proof support, not for the correctness proof
of refinement mappings!
- Note: Everything is superseded by @{file "LiveIOA.thy"}.
+ Note: Everything is superseded by \<^file>\<open>LiveIOA.thy\<close>.
\<close>
axiomatization where
--- a/src/HOL/HOLCF/IOA/Traces.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/HOLCF/IOA/Traces.thy Fri Aug 12 20:58:20 2016 +0200
@@ -84,7 +84,7 @@
else branch prohibits it. However they can be \<open>sfair\<close> in the case when all
\<open>W\<close> are only finitely often enabled: Is this the right model?
- See @{file "LiveIOA.thy"} for solution conforming with the literature and
+ See \<^file>\<open>LiveIOA.thy\<close> for solution conforming with the literature and
superseding this one.
\<close>
--- a/src/HOL/Imperative_HOL/Ref.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Imperative_HOL/Ref.thy Fri Aug 12 20:58:20 2016 +0200
@@ -10,8 +10,8 @@
text \<open>
Imperative reference operations; modeled after their ML counterparts.
- See @{url "http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html"}
- and @{url "http://www.smlnj.org/doc/Conversion/top-level-comparison.html"}
+ See \<^url>\<open>http://caml.inria.fr/pub/docs/manual-caml-light/node14.15.html\<close>
+ and \<^url>\<open>http://www.smlnj.org/doc/Conversion/top-level-comparison.html\<close>.
\<close>
subsection \<open>Primitives\<close>
--- a/src/HOL/Induct/Ordinals.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Induct/Ordinals.thy Fri Aug 12 20:58:20 2016 +0200
@@ -11,7 +11,7 @@
text \<open>
Some basic definitions of ordinal numbers. Draws an Agda
development (in Martin-L\"of type theory) by Peter Hancock (see
- @{url "http://www.dcs.ed.ac.uk/home/pgh/chat.html"}).
+ \<^url>\<open>http://www.dcs.ed.ac.uk/home/pgh/chat.html\<close>).
\<close>
datatype ordinal =
--- a/src/HOL/Isar_Examples/Cantor.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Isar_Examples/Cantor.thy Fri Aug 12 20:58:20 2016 +0200
@@ -13,8 +13,8 @@
text \<open>
Cantor's Theorem states that there is no surjection from
a set to its powerset. The proof works by diagonalization. E.g.\ see
- \<^item> @{url "http://mathworld.wolfram.com/CantorDiagonalMethod.html"}
- \<^item> @{url "https://en.wikipedia.org/wiki/Cantor's_diagonal_argument"}
+ \<^item> \<^url>\<open>http://mathworld.wolfram.com/CantorDiagonalMethod.html\<close>
+ \<^item> \<^url>\<open>https://en.wikipedia.org/wiki/Cantor's_diagonal_argument\<close>
\<close>
theorem Cantor: "\<nexists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. A = f x"
--- a/src/HOL/Isar_Examples/Hoare.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Isar_Examples/Hoare.thy Fri Aug 12 20:58:20 2016 +0200
@@ -16,7 +16,7 @@
The following abstract syntax and semantics of Hoare Logic over \<^verbatim>\<open>WHILE\<close>
programs closely follows the existing tradition in Isabelle/HOL of
formalizing the presentation given in @{cite \<open>\S6\<close> "Winskel:1993"}. See also
- @{file "~~/src/HOL/Hoare"} and @{cite "Nipkow:1998:Winskel"}.
+ \<^dir>\<open>~~/src/HOL/Hoare\<close> and @{cite "Nipkow:1998:Winskel"}.
\<close>
type_synonym 'a bexp = "'a set"
@@ -358,14 +358,14 @@
text \<open>
We now load the \<^emph>\<open>original\<close> ML file for proof scripts and tactic definition
- for the Hoare Verification Condition Generator (see @{file
- "~~/src/HOL/Hoare/"}). As far as we are concerned here, the result is a
- proof method \<open>hoare\<close>, which may be applied to a Hoare Logic assertion to
- extract purely logical verification conditions. It is important to note that
- the method requires \<^verbatim>\<open>WHILE\<close> loops to be fully annotated with invariants
- beforehand. Furthermore, only \<^emph>\<open>concrete\<close> pieces of code are handled --- the
- underlying tactic fails ungracefully if supplied with meta-variables or
- parameters, for example.
+ for the Hoare Verification Condition Generator (see \<^dir>\<open>~~/src/HOL/Hoare\<close>).
+ As far as we are concerned here, the result is a proof method \<open>hoare\<close>, which
+ may be applied to a Hoare Logic assertion to extract purely logical
+ verification conditions. It is important to note that the method requires
+ \<^verbatim>\<open>WHILE\<close> loops to be fully annotated with invariants beforehand.
+ Furthermore, only \<^emph>\<open>concrete\<close> pieces of code are handled --- the underlying
+ tactic fails ungracefully if supplied with meta-variables or parameters, for
+ example.
\<close>
lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
--- a/src/HOL/Isar_Examples/Schroeder_Bernstein.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Isar_Examples/Schroeder_Bernstein.thy Fri Aug 12 20:58:20 2016 +0200
@@ -10,8 +10,8 @@
text \<open>
See also:
- \<^item> @{file "$ISABELLE_HOME/src/HOL/ex/Set_Theory.thy"}
- \<^item> @{url "http://planetmath.org/proofofschroederbernsteintheoremusingtarskiknastertheorem"}
+ \<^item> \<^file>\<open>$ISABELLE_HOME/src/HOL/ex/Set_Theory.thy\<close>
+ \<^item> \<^url>\<open>http://planetmath.org/proofofschroederbernsteintheoremusingtarskiknastertheorem\<close>
\<^item> Springer LNCS 828 (cover page)
\<close>
--- a/src/HOL/Library/Code_Test.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Library/Code_Test.thy Fri Aug 12 20:58:20 2016 +0200
@@ -53,9 +53,10 @@
and (Scala) "_.mkString(\"\")"
text \<open>
- Stripped-down implementations of Isabelle's XML tree with YXML encoding
- as defined in @{file "~~/src/Pure/PIDE/xml.ML"}, @{file "~~/src/Pure/PIDE/yxml.ML"}
- sufficient to encode @{typ "Code_Evaluation.term"} as in @{file "~~/src/Pure/term_xml.ML"}.
+ Stripped-down implementations of Isabelle's XML tree with YXML encoding as
+ defined in \<^file>\<open>~~/src/Pure/PIDE/xml.ML\<close>, \<^file>\<open>~~/src/Pure/PIDE/yxml.ML\<close>
+ sufficient to encode @{typ "Code_Evaluation.term"} as in
+ \<^file>\<open>~~/src/Pure/term_xml.ML\<close>.
\<close>
datatype (plugins del: code size "quickcheck") xml_tree = XML_Tree
@@ -113,8 +114,8 @@
where "yxml_string_of_body ts = foldr yxml_string_of_xml_tree ts yot_empty"
text \<open>
- Encoding @{typ Code_Evaluation.term} into XML trees
- as defined in @{file "~~/src/Pure/term_xml.ML"}
+ Encoding @{typ Code_Evaluation.term} into XML trees as defined in
+ \<^file>\<open>~~/src/Pure/term_xml.ML\<close>.
\<close>
definition xml_of_typ :: "Typerep.typerep \<Rightarrow> xml.body"
--- a/src/HOL/Library/Extended_Real.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Library/Extended_Real.thy Fri Aug 12 20:58:20 2016 +0200
@@ -218,10 +218,8 @@
qed
text \<open>
-
-For more lemmas about the extended real numbers go to
- @{file "~~/src/HOL/Analysis/Extended_Real_Limits.thy"}
-
+ For more lemmas about the extended real numbers see
+ \<^file>\<open>~~/src/HOL/Analysis/Extended_Real_Limits.thy\<close>.
\<close>
subsection \<open>Definition and basic properties\<close>
--- a/src/HOL/Library/RBT_Impl.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Library/RBT_Impl.thy Fri Aug 12 20:58:20 2016 +0200
@@ -551,8 +551,10 @@
lemma bheight_paintR'[simp]: "color_of t = B \<Longrightarrow> bheight (paint R t) = bheight t - 1"
by (cases t rule: rbt_cases) auto
-text \<open>The function definitions are based on the Haskell code by Stefan Kahrs
-at @{url "http://www.cs.ukc.ac.uk/people/staff/smk/redblack/rb.html"} .\<close>
+text \<open>
+ The function definitions are based on the Haskell code by Stefan Kahrs
+ at \<^url>\<open>http://www.cs.ukc.ac.uk/people/staff/smk/redblack/rb.html\<close>.
+\<close>
fun
balance_left :: "('a,'b) rbt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a,'b) rbt \<Rightarrow> ('a,'b) rbt"
--- a/src/HOL/Library/Set_Algebras.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Library/Set_Algebras.thy Fri Aug 12 20:58:20 2016 +0200
@@ -13,7 +13,7 @@
text \<open>
This library lifts operations like addition and multiplication to sets. It
was designed to support asymptotic calculations. See the comments at the top
- of @{file "BigO.thy"}.
+ of \<^file>\<open>BigO.thy\<close>.
\<close>
instantiation set :: (plus) plus
--- a/src/HOL/Library/State_Monad.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Library/State_Monad.thy Fri Aug 12 20:58:20 2016 +0200
@@ -20,7 +20,7 @@
monads}, since a state is transformed single-threadedly).
To enter from the Haskell world,
- @{url "http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm"} makes
+ \<^url>\<open>http://www.engr.mun.ca/~theo/Misc/haskell_and_monads.htm\<close> makes
a good motivating start. Here we just sketch briefly how those
monads enter the game of Isabelle/HOL.
\<close>
@@ -145,7 +145,7 @@
"_sdo_block (_sdo_final e)" => "e"
text \<open>
- For an example, see @{file "~~/src/HOL/Proofs/Extraction/Higman_Extraction.thy"}.
+ For an example, see \<^file>\<open>~~/src/HOL/Proofs/Extraction/Higman_Extraction.thy\<close>.
\<close>
end
--- a/src/HOL/Library/positivstellensatz.ML Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Fri Aug 12 20:58:20 2016 +0200
@@ -495,7 +495,7 @@
val P = Thm.lhs_of PQ
in Thm.implies_intr P (Thm.equal_elim PQ (Thm.assume P))
end
- (* FIXME!!! Copied from groebner.ml *)
+ (*FIXME!!! Copied from groebner.ml*)
val strip_exists =
let
fun h (acc, t) =
--- a/src/HOL/Nominal/Examples/CK_Machine.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Nominal/Examples/CK_Machine.thy Fri Aug 12 20:58:20 2016 +0200
@@ -16,9 +16,8 @@
by Roshan James (Indiana University) and also by the lecture notes
written by Andy Pitts for his semantics course. See
- @{url "http://www.cs.indiana.edu/~rpjames/lm.pdf"}
- @{url "http://www.cl.cam.ac.uk/teaching/2001/Semantics/"}
-
+ \<^url>\<open>http://www.cs.indiana.edu/~rpjames/lm.pdf\<close>
+ \<^url>\<open>http://www.cl.cam.ac.uk/teaching/2001/Semantics\<close>
\<close>
atom_decl name
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Fri Aug 12 20:58:20 2016 +0200
@@ -4,7 +4,7 @@
"~~/src/HOL/Library/Code_Prolog"
begin
-text \<open>An example from the experiments from SmallCheck (@{url "http://www.cs.york.ac.uk/fp/smallcheck/"})\<close>
+text \<open>An example from the experiments from SmallCheck (\<^url>\<open>http://www.cs.york.ac.uk/fp/smallcheck\<close>)\<close>
text \<open>The example (original in Haskell) was imported with Haskabelle and
manually slightly adapted.
\<close>
--- a/src/HOL/Probability/Probability_Mass_Function.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Fri Aug 12 20:58:20 2016 +0200
@@ -1414,7 +1414,7 @@
Proof that @{const rel_pmf} preserves orders.
Antisymmetry proof follows Thm. 1 in N. Saheb-Djahromi, Cpo's of measures for nondeterminism,
Theoretical Computer Science 12(1):19--37, 1980,
- @{url "http://dx.doi.org/10.1016/0304-3975(80)90003-1"}
+ \<^url>\<open>http://dx.doi.org/10.1016/0304-3975(80)90003-1\<close>
\<close>
lemma
--- a/src/HOL/Real.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Real.thy Fri Aug 12 20:58:20 2016 +0200
@@ -14,10 +14,10 @@
begin
text \<open>
- This theory contains a formalization of the real numbers as
- equivalence classes of Cauchy sequences of rationals. See
- @{file "~~/src/HOL/ex/Dedekind_Real.thy"} for an alternative
- construction using Dedekind cuts.
+ This theory contains a formalization of the real numbers as equivalence
+ classes of Cauchy sequences of rationals. See
+ \<^file>\<open>~~/src/HOL/ex/Dedekind_Real.thy\<close> for an alternative construction using
+ Dedekind cuts.
\<close>
--- a/src/HOL/Real_Vector_Spaces.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Fri Aug 12 20:58:20 2016 +0200
@@ -2084,7 +2084,7 @@
text \<open>
Proof that Cauchy sequences converge based on the one from
- @{url "http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html"}
+ \<^url>\<open>http://pirate.shu.edu/~wachsmut/ira/numseq/proofs/cauconv.html\<close>
\<close>
text \<open>
--- a/src/HOL/Rings.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Rings.thy Fri Aug 12 20:58:20 2016 +0200
@@ -538,7 +538,7 @@
\<^item> \<^emph>\<open>Partially Ordered Algebraic Systems\<close>, Pergamon Press, 1963
Most of the used notions can also be looked up in
- \<^item> @{url "http://www.mathworld.com"} by Eric Weisstein et. al.
+ \<^item> \<^url>\<open>http://www.mathworld.com\<close> by Eric Weisstein et. al.
\<^item> \<^emph>\<open>Algebra I\<close> by van der Waerden, Springer
\<close>
--- a/src/HOL/Series.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Series.thy Fri Aug 12 20:58:20 2016 +0200
@@ -817,7 +817,7 @@
text \<open>
Proof based on Analysis WebNotes: Chapter 07, Class 41
- @{url "http://www.math.unl.edu/~webnotes/classes/class41/prp77.htm"}
+ \<^url>\<open>http://www.math.unl.edu/~webnotes/classes/class41/prp77.htm\<close>
\<close>
lemma Cauchy_product_sums:
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Aug 12 20:58:20 2016 +0200
@@ -199,10 +199,10 @@
(** invocation of Haskell interpreter **)
val narrowing_engine =
- File.read @{path "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs"}
+ File.read \<^file>\<open>~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs\<close>
val pnf_narrowing_engine =
- File.read @{path "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"}
+ File.read \<^file>\<open>~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs\<close>
fun exec verbose code =
ML_Context.exec (fn () =>
--- a/src/HOL/Word/Word.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/Word/Word.thy Fri Aug 12 20:58:20 2016 +0200
@@ -14,7 +14,7 @@
Word_Miscellaneous
begin
-text \<open>See @{file "Examples/WordExamples.thy"} for examples.\<close>
+text \<open>See \<^file>\<open>Examples/WordExamples.thy\<close> for examples.\<close>
subsection \<open>Type definition\<close>
--- a/src/HOL/ex/ML.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/ex/ML.thy Fri Aug 12 20:58:20 2016 +0200
@@ -94,7 +94,7 @@
ML \<open>factorial 42\<close>
ML \<open>factorial 10000 div factorial 9999\<close>
-text \<open>See @{url "http://mathworld.wolfram.com/AckermannFunction.html"}\<close>
+text \<open>See \<^url>\<open>http://mathworld.wolfram.com/AckermannFunction.html\<close>.\<close>
ML \<open>
fun ackermann 0 n = n + 1
--- a/src/HOL/ex/NatSum.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/ex/NatSum.thy Fri Aug 12 20:58:20 2016 +0200
@@ -10,7 +10,7 @@
Summing natural numbers, squares, cubes, etc.
Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
- @{url "http://www.research.att.com/~njas/sequences/"}.
+ \<^url>\<open>http://www.research.att.com/~njas/sequences\<close>.
\<close>
lemmas [simp] =
--- a/src/HOL/ex/Simproc_Tests.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/ex/Simproc_Tests.thy Fri Aug 12 20:58:20 2016 +0200
@@ -9,10 +9,9 @@
begin
text \<open>
- This theory tests the various simprocs defined in @{file
- "~~/src/HOL/Nat.thy"} and @{file "~~/src/HOL/Numeral_Simprocs.thy"}.
- Many of the tests are derived from commented-out code originally
- found in @{file "~~/src/HOL/Tools/numeral_simprocs.ML"}.
+ This theory tests the various simprocs defined in \<^file>\<open>~~/src/HOL/Nat.thy\<close> and
+ \<^file>\<open>~~/src/HOL/Numeral_Simprocs.thy\<close>. Many of the tests are derived from commented-out code
+ originally found in \<^file>\<open>~~/src/HOL/Tools/numeral_simprocs.ML\<close>.
\<close>
subsection \<open>ML bindings\<close>
--- a/src/HOL/ex/Sudoku.thy Fri Aug 12 18:08:40 2016 +0200
+++ b/src/HOL/ex/Sudoku.thy Fri Aug 12 20:58:20 2016 +0200
@@ -136,7 +136,7 @@
text \<open>
Some ``exceptionally difficult'' Sudokus, taken from
- @{url "http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903"}
+ \<^url>\<open>http://en.wikipedia.org/w/index.php?title=Algorithmics_of_sudoku&oldid=254685903\<close>
(accessed December~2, 2008).
\<close>
--- a/src/Pure/General/file.ML Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Pure/General/file.ML Fri Aug 12 20:58:20 2016 +0200
@@ -98,11 +98,11 @@
fun check_dir path =
if exists path andalso is_dir path then path
- else error ("No such directory: " ^ Path.print path);
+ else error ("No such directory: " ^ Path.print (Path.expand path));
fun check_file path =
if exists path andalso not (is_dir path) then path
- else error ("No such file: " ^ Path.print path);
+ else error ("No such file: " ^ Path.print (Path.expand path));
(* open streams *)
--- a/src/Pure/Isar/document_structure.scala Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Pure/Isar/document_structure.scala Fri Aug 12 20:58:20 2016 +0200
@@ -190,10 +190,15 @@
toks.filterNot(_.is_space) match {
case List(tok) if tok.is_comment =>
val s = tok.source
- if (s.startsWith("(**** ") && s.endsWith(" ****)")) Some(0)
- else if (s.startsWith("(*** ") && s.endsWith(" ***)")) Some(1)
- else if (s.startsWith("(** ") && s.endsWith(" **)")) Some(2)
- else if (s.startsWith("(* ") && s.endsWith(" *)")) Some(3)
+ if (Word.codepoint_iterator(s).exists(c =>
+ Character.isLetter(c) || Character.isDigit(c)))
+ {
+ if (s.startsWith("(**** ") && s.endsWith(" ****)")) Some(0)
+ else if (s.startsWith("(*** ") && s.endsWith(" ***)")) Some(1)
+ else if (s.startsWith("(** ") && s.endsWith(" **)")) Some(2)
+ else if (s.startsWith("(* ") && s.endsWith(" *)")) Some(3)
+ else None
+ }
else None
case _ => None
}
--- a/src/Pure/Isar/parse.ML Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Pure/Isar/parse.ML Fri Aug 12 20:58:20 2016 +0200
@@ -270,7 +270,7 @@
val text = group (fn () => "text") (embedded || verbatim);
-val path = group (fn () => "file name/path specification") name;
+val path = group (fn () => "file name/path specification") embedded;
val theory_name = group (fn () => "theory name") name;
--- a/src/Pure/ML/ml_context.ML Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Pure/ML/ml_context.ML Fri Aug 12 20:58:20 2016 +0200
@@ -96,7 +96,7 @@
local
val antiq =
- Parse.!!! ((Parse.token Parse.name ::: Parse.args) --| Scan.ahead Parse.eof);
+ Parse.!!! ((Parse.token Parse.liberal_name ::: Parse.args) --| Scan.ahead Parse.eof);
fun make_env name visible =
(ML_Lex.tokenize
--- a/src/Pure/PIDE/markup.ML Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Pure/PIDE/markup.ML Fri Aug 12 20:58:20 2016 +0200
@@ -189,6 +189,7 @@
val padding_line: Properties.entry
val padding_command: Properties.entry
val dialogN: string val dialog: serial -> string -> T
+ val jedit_actionN: string
val functionN: string
val assign_update: Properties.T
val removed_versions: Properties.T
@@ -636,6 +637,8 @@
val dialogN = "dialog";
fun dialog i result = (dialogN, [(serialN, print_int i), (resultN, result)]);
+val jedit_actionN = "jedit_action";
+
(* protocol message functions *)
--- a/src/Pure/PIDE/markup.scala Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Pure/PIDE/markup.scala Fri Aug 12 20:58:20 2016 +0200
@@ -472,6 +472,8 @@
val DIALOG = "dialog"
val Result = new Properties.String(RESULT)
+ val JEDIT_ACTION = "jedit_action"
+
/* protocol message functions */
--- a/src/Pure/PIDE/resources.ML Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Pure/PIDE/resources.ML Fri Aug 12 20:58:20 2016 +0200
@@ -184,33 +184,25 @@
local
-fun check_path strict ctxt dir (name, pos) =
+fun err msg pos = error (msg ^ Position.here pos);
+
+fun check_path check_file ctxt dir (name, pos) =
let
val _ = Context_Position.report ctxt pos Markup.language_path;
- val path = Path.append dir (Path.explode name)
- handle ERROR msg => error (msg ^ Position.here pos);
-
+ val path = Path.append dir (Path.explode name) handle ERROR msg => err msg pos;
+ val _ = Path.expand path handle ERROR msg => err msg pos;
val _ = Context_Position.report ctxt pos (Markup.path (Path.smart_implode path));
val _ =
- if can Path.expand path andalso File.exists path then ()
- else
- let
- val path' = perhaps (try Path.expand) path;
- val msg = "Bad file: " ^ Path.print path' ^ Position.here pos;
- in
- if strict then error msg
- else if Context_Position.is_visible ctxt then
- Output.report
- [Markup.markup (Markup.bad |> Markup.properties (Position.properties_of pos)) msg]
- else ()
- end;
+ (case check_file of
+ NONE => path
+ | SOME check => (check path handle ERROR msg => err msg pos));
in path end;
-fun file_antiq strict ctxt (name, pos) =
+fun document_antiq check_file ctxt (name, pos) =
let
val dir = master_directory (Proof_Context.theory_of ctxt);
- val _ = check_path strict ctxt dir (name, pos);
+ val _ = check_path check_file ctxt dir (name, pos);
in
space_explode "/" name
|> map Latex.output_ascii
@@ -218,17 +210,28 @@
|> enclose "\\isatt{" "}"
end;
+fun ML_antiq check_file ctxt (name, pos) =
+ let val path = check_path check_file ctxt Path.current (name, pos);
+ in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end;
+
in
val _ = Theory.setup
- (Thy_Output.antiquotation @{binding file} (Scan.lift (Parse.position Parse.path))
- (file_antiq true o #context) #>
- Thy_Output.antiquotation @{binding file_unchecked} (Scan.lift (Parse.position Parse.path))
- (file_antiq false o #context) #>
+ (Thy_Output.antiquotation @{binding path} (Scan.lift (Parse.position Parse.path))
+ (document_antiq NONE o #context) #>
+ Thy_Output.antiquotation @{binding file} (Scan.lift (Parse.position Parse.path))
+ (document_antiq (SOME File.check_file) o #context) #>
+ Thy_Output.antiquotation @{binding dir} (Scan.lift (Parse.position Parse.path))
+ (document_antiq (SOME File.check_dir) o #context) #>
ML_Antiquotation.value @{binding path}
- (Args.context -- Scan.lift (Parse.position Parse.path) >> (fn (ctxt, arg) =>
- let val path = check_path true ctxt Path.current arg
- in "Path.explode " ^ ML_Syntax.print_string (Path.implode path) end)));
+ (Args.context -- Scan.lift (Parse.position Parse.path)
+ >> uncurry (ML_antiq NONE)) #>
+ ML_Antiquotation.value @{binding file}
+ (Args.context -- Scan.lift (Parse.position Parse.path)
+ >> uncurry (ML_antiq (SOME File.check_file))) #>
+ ML_Antiquotation.value @{binding dir}
+ (Args.context -- Scan.lift (Parse.position Parse.path)
+ >> uncurry (ML_antiq (SOME File.check_dir))));
end;
--- a/src/Pure/Thy/document_antiquotations.ML Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML Fri Aug 12 20:58:20 2016 +0200
@@ -204,7 +204,7 @@
(* doc entries *)
val _ = Theory.setup
- (Thy_Output.antiquotation @{binding doc} (Scan.lift (Parse.position Parse.name))
+ (Thy_Output.antiquotation @{binding doc} (Scan.lift (Parse.position Parse.embedded))
(fn {context = ctxt, ...} => fn (name, pos) =>
(Context_Position.report ctxt pos (Markup.doc name);
Thy_Output.output ctxt [Thy_Output.pretty_text ctxt name])));
--- a/src/Pure/Tools/jedit.ML Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Pure/Tools/jedit.ML Fri Aug 12 20:58:20 2016 +0200
@@ -24,13 +24,13 @@
val isabelle_jedit_actions =
Lazy.lazy (fn () =>
- (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of
+ (case XML.parse (File.read \<^file>\<open>~~/src/Tools/jEdit/src/actions.xml\<close>) of
XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body
| _ => []));
val isabelle_jedit_dockables =
Lazy.lazy (fn () =>
- (case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of
+ (case XML.parse (File.read \<^file>\<open>~~/src/Tools/jEdit/src/dockables.xml\<close>) of
XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body
| _ => []));
@@ -53,7 +53,13 @@
in
fun check_action (name, pos) =
- if member (op =) (Lazy.force all_actions) name then name
+ if member (op =) (Lazy.force all_actions) name then
+ let
+ val ((bg1, bg2), en) =
+ YXML.output_markup_elem
+ (Active.make_markup Markup.jedit_actionN {implicit = false, properties = []});
+ val msg = "Invoke " ^ bg1 ^ name ^ bg2 ^ name ^ en ^ " jEdit action";
+ in writeln (msg ^ Position.here pos); name end
else
let
val completion =
@@ -66,6 +72,13 @@
val report = Markup.markup_report (Completion.reported_text completion);
in error ("Bad jEdit action " ^ quote name ^ Position.here pos ^ report) end
+val _ =
+ Theory.setup
+ (Thy_Output.antiquotation @{binding action} (Scan.lift (Parse.position Parse.embedded))
+ (fn {context = ctxt, ...} => fn (name, pos) =>
+ (if Context_Position.is_reported ctxt pos then ignore (check_action (name, pos)) else ();
+ Thy_Output.verbatim_text ctxt name)));
+
end;
end;
--- a/src/Tools/jEdit/src/active.scala Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Tools/jEdit/src/active.scala Fri Aug 12 20:58:20 2016 +0200
@@ -43,6 +43,11 @@
GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) }
}
+ case XML.Elem(Markup(Markup.JEDIT_ACTION, _), body) =>
+ GUI_Thread.later {
+ view.getInputHandler.invokeAction(XML.content(body))
+ }
+
case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, props), _) =>
val link =
props match {
--- a/src/Tools/jEdit/src/completion_popup.scala Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Fri Aug 12 20:58:20 2016 +0200
@@ -222,11 +222,16 @@
catch { case ERROR(_) => Nil }
}
+ def is_wrapped(s: String): Boolean =
+ s.startsWith("\"") && s.endsWith("\"") ||
+ s.startsWith(Symbol.open_decoded) && s.endsWith(Symbol.close_decoded)
+
for {
r1 <- rendering.language_path(JEdit_Lib.before_caret_range(text_area, rendering))
s1 <- JEdit_Lib.try_get_text(text_area.getBuffer, r1)
- s2 <- Library.try_unquote(s1)
+ if is_wrapped(s1)
r2 = Text.Range(r1.start + 1, r1.stop - 1)
+ s2 = s1.substring(1, s1.length - 1)
if Path.is_valid(s2)
paths = complete(s2)
if paths.nonEmpty
--- a/src/Tools/jEdit/src/rendering.scala Fri Aug 12 18:08:40 2016 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Fri Aug 12 20:58:20 2016 +0200
@@ -169,7 +169,7 @@
private val active_elements =
Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
- Markup.SENDBACK, Markup.SIMP_TRACE_PANEL)
+ Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL)
private val tooltip_message_elements =
Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,