home *** CD-ROM | disk | FTP | other *** search
/ Mega Top 1 / os2_top1.zip / os2_top1 / APPS / TEKST / ZEMTEX / TEXINPUT.ZIP / OZ.STY < prev   
Text File  |  1993-03-02  |  44KB  |  1,347 lines

  1. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  2. %
  3. % oz.sty
  4. %
  5. \message{`OZ Macros' <10 Apr 91>}
  6. %
  7. %    This document is organised as follows:
  8. %
  9. %    SECTION 1    Z FONTS
  10. %    SECTION 2    Z SYMBOLS
  11. %    SECTION 3    Z ENVIRONMENTS
  12. %
  13. % Modification History:
  14. %
  15. %               The original zed.sty file was written by Mike Spivey.
  16. %               These macros have been extensively modified to
  17. %               include extra symbols and environments for Object-Z
  18. %               and now have little resemblence to the original macros.
  19. %               Mike Spivey has also extended his macros along
  20. %               different lines for Z - the latest version of macros
  21. %               are called fuzz.sty and come with a syntax checker for Z.
  22. %               They can be purchased for a small fee from:
  23. %                       mike@prg.oxford.ac.uk
  24. %
  25. %        87    original zed.sty file - Mike Spivey
  26. %        88    modified to include extra symbols and environments - Paul King
  27. %        88    modified to include macros for UQ editor - Ray Neucom
  28. %    May 89    modified to include object-oriented constructs - PK
  29. %    Jun 89    modified to automatically change Z symbol size - PK
  30. % 27 Jul 89    removed spurious space from \@setsize - PK
  31. %  3 Aug 89    adjust style of equation number field - PK
  32. % 24 Aug 89     add optional field to topline and zedline for proofs - PK
  33. % 15 Sep 89     added extra qed symbols, updated classcom and comment - PK
  34. % 25 Sep 89    renamed z@[bB]ig to z[bB]ig and changed temporal symbols - PK
  35. % 30 Sep 89    added \znewpage, \Infrule, removed space above state box - PK
  36. % 12 Mar 90    changed \@setsize to work better for double-spaced text - PK
  37. % 31 Mar 90    added definition for @ and \bool and redefined `;' - PK
  38. %  9 May 90    changed \sdef to \varsdef, \sdef & \defs to Spivey's latest - PK
  39. % 27 May 90    added \c{n}{text} - a tab like \t{n} with text at left - PK
  40. % 29 May 90    added `corners' to boxes and \zedcornerheight - PK
  41. % 11 Jul 90    added \rename*[y/x] and \zseq \zset ..., changed \zeq \zimp - PK
  42. %  2 Aug 90     added \subseq, \iseq - PK
  43. %  9 Nov 90    changed \M to hopefully interact better with spacing - PK
  44. % 18 Dec 90    changed to new AMS 2.0 fonts - PK (with help from Adrian Lee)
  45. % 11 Feb 91    added \poly \widen and modified \gendef - PK
  46. % 10 Apr 91    added \fuzzcompatible - PK
  47. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  48. % Please post any updates that you may make to this file to:
  49. %    Paul King -- ACSnet: king@batserver.cs.uq.oz.au
  50. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  51. % Thanks to the following people for making suggestions/comments about oz.sty:
  52. %    Jim Grundy (jg@computer-lab.cambridge.ac.uk)
  53. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  54. %
  55. %    SECTION 1    Z FONTS
  56. %
  57. % The AMS extra symbol fonts are loaded.
  58. %    Note: msam and msbm used to be called msxm and msym and before that
  59. %          euxm and euym respectively.
  60. %             You may need to do some renaming if you don't have the latest
  61. %          version of the AMS fonts (2.0).
  62. %
  63. % The MetaFont sources (mf files) for the AMS 2.0 fonts are
  64. % available for anonymous ftp from:
  65. %
  66. % address:    labrea.stanford.edu (36.8.0.47)
  67. % files:    pub/tex/ams/amsfonts/sources/symbols/*
  68. %
  69. %
  70. %\font\fivmsx=msam5
  71. \font\fivmsx=msam5.tfm
  72. \font\fivmsy=msbm5.tfm
  73. \font\sixmsx=msam6.tfm
  74. %
  75. %\font\fivmsy=msbm5
  76. %\font\sixmsx=msam6
  77. %
  78. \font\sixmsy=msbm6
  79. \font\sevmsx=msam7
  80. \font\sevmsy=msbm7
  81. \font\egtmsx=msam8            \font\egtmsy=msbm8
  82. \font\ninmsx=msam9            \font\ninmsy=msbm9
  83. \font\tenmsx=msam10            \font\tenmsy=msbm10
  84. \font\elvmsx=msam10 \@halfmag        \font\elvmsy=msbm10 \@halfmag
  85. \font\twlmsx=msam10 \@magscale1        \font\twlmsy=msbm10 \@magscale1
  86. \font\frtnmsx=msam10 \@magscale2    \font\frtnmsy=msbm10 \@magscale2
  87. \font\svtnmsx=msam10 \@magscale3    \font\svtnmsy=msbm10 \@magscale3
  88. \font\twtymsx=msam10 \@magscale4    \font\twtymsy=msbm10 \@magscale4
  89. \font\twfvmsx=msam10 \@magscale5    \font\twfvmsy=msbm10 \@magscale5
  90.  
  91. %
  92. % Load fonts not normally loaded
  93. %
  94. \font\frtnit=cmti10\@magscale2
  95. \font\svtnit=cmti10\@magscale3
  96. \font\twtyit=cmti10\@magscale4
  97. \font\twfvit=cmti10\@magscale5
  98. \font\twfvsy=cmsy10\@magscale5
  99. \font\twtybf=cmbx10\@magscale4
  100. \font\twfvbf=cmbx10\@magscale5
  101.  
  102. \newfam\msxfam
  103. \newfam\msyfam
  104.  
  105. %
  106. % Now make size changing commands automatically change size of Z symbols
  107. % Doesn't work for letters in the cmex fonts e.g. \bigcup, \sum
  108. %
  109. \def\@vpt{\textfont\msxfam=\fivmsx
  110.     \textfont\msyfam=\fivmsy}
  111. %
  112. \def\@vipt{\textfont\msxfam=\sixmsx
  113.     \textfont\msyfam=\sixmsy}
  114. %
  115. \def\@viipt{\textfont\msxfam=\sevmsx
  116.     \textfont\msyfam=\sevmsy}
  117. %
  118. \def\@viiipt{\textfont\msxfam=\egtmsx
  119.     \textfont\msyfam=\egtmsy}
  120. %
  121. \def\@ixpt{\textfont\msxfam=\ninmsx \scriptfont\msxfam=\sixmsx
  122.     \textfont\msyfam=\ninmsy \scriptfont\msyfam=\sixmsy}
  123. %
  124. \def\@xpt{\textfont\msxfam=\tenmsx \scriptfont\msxfam=\sevmsx
  125.     \textfont\msyfam=\tenmsy \scriptfont\msyfam=\sevmsy}
  126. %
  127. \def\@xipt{\textfont\msxfam=\elvmsx \scriptfont\msxfam=\egtmsx
  128.     \textfont\msyfam=\elvmsy \scriptfont\msyfam=\egtmsy}
  129. %
  130. \def\@xiipt{\textfont\msxfam=\twlmsx \scriptfont\msxfam=\ninmsx
  131.     \textfont\msyfam=\twlmsy \scriptfont\msyfam=\ninmsy}
  132. %
  133. \def\@xivpt{\textfont\msxfam=\frtnmsx \scriptfont\msxfam=\tenmsx
  134.     \textfont\msyfam=\frtnmsy \scriptfont\msyfam=\tenmsy
  135.     \textfont\itfam=\frtnit \scriptfont\itfam=\tenit}
  136. %
  137. \def\@xviipt{\textfont\msxfam=\svtnmsx \scriptfont\msxfam=\twlmsx
  138.     \textfont\msyfam=\svtnmsy \scriptfont\msyfam=\twlmsy
  139.     \textfont\itfam=\svtnit \scriptfont\itfam=\twlit}
  140. %
  141. \def\@xxpt{\textfont\msxfam=\twtymsx \scriptfont\msxfam=\frtnmsx
  142.     \textfont\msyfam=\twtymsy \scriptfont\msyfam=\frtnmsy
  143.     \textfont\bffam=\twtybf
  144.     \textfont\itfam=\twtyit \scriptfont\itfam=\frtnit}
  145. %
  146. \def\@xxvpt{\textfont\msxfam=\twfvmsx \scriptfont\msxfam=\svtnmsx
  147.     \textfont\msyfam=\twfvmsy \scriptfont\msyfam=\svtnmsy
  148.     \textfont\itfam=\twtyit \scriptfont\itfam=\svtnit
  149.     \textfont\bffam=\twfvbf \scriptfont\tw@=\svtnsy}
  150. %
  151.  
  152. \def\bbold{\fam\msyfam}
  153. \def\@famletter#1{\ifcase #1 0\or 1\or 2\or 3\or 4\or 5\or 6\or 7\or
  154.     8\or 9\or A\or B\or C\or D\or E\or F\fi}
  155.  
  156. \edef\@fx{\@famletter\msxfam}
  157. \edef\@fy{\@famletter\msyfam}
  158.  
  159. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  160. %
  161. %    SECTION 2    Z SYMBOLS
  162. %
  163. % The mathcodes for the letters A, ..., Z, a, ..., z are changed to
  164. % generate text italic rather than math italic by default. This makes
  165. % multi-letter identifiers look better. The mathcode for character c
  166. % is set to "7000 (variable family) + "400 (text italic) + c.
  167. %
  168.  
  169. \def\@setmcodes#1#2#3{{\count0=#1 \count1=#3
  170.     \loop \global\mathcode\count0=\count1 \ifnum \count0<#2
  171.     \advance\count0 by1 \advance\count1 by1 \repeat}}
  172.  
  173. \@setmcodes{`A}{`Z}{"7441}
  174. \@setmcodes{`a}{`z}{"7461}
  175. %
  176. % Also, the mathcode for semicolon is set to "8000, so it behaves as an
  177. % active character in math mode; it is defined to insert a thick space.
  178. % \semicolon is a semicolon as an ordinary symbol.
  179. %
  180. \let\@mc=\mathchardef
  181. \mathcode`\;="8000 % Makes ; active in math mode
  182. {\catcode`\;=\active \gdef;{\semicolon\;}}
  183. \@mc\semicolon="603B
  184.  
  185. %
  186. %        ------ UTILITY MACROS FOR Z SYMBOLS ------
  187. %
  188.  
  189. % \z@op        makes a large math operator
  190. % \z@rel    makes a math relation
  191. % \z@bin    makes a binary operator
  192. %
  193. % each use a mathstrut to defeat TeX's vertical adjustment.
  194. % \z@bigXXX big version of symbol
  195. %
  196. \def\z@op#1{\mathop{\mathstrut{#1}}\nolimits}
  197. \def\z@bin#1{\mathbin{\mathstrut{#1}}}
  198. \def\z@rel#1{\mathrel{\mathstrut{#1}}}
  199. %
  200. \def\z@bigop#1{\z@op{\zbig{#1}}}
  201. \def\z@bigbin#1{\z@bin{\zbig{#1}}}
  202. \def\z@bigrel#1{\z@rel{\zbig{#1}}}
  203. %
  204. \def\z@Bigop#1{\z@op{\zBig{#1}}}
  205. \def\z@Bigbin#1{\z@bin{\zBig{#1}}}
  206. \def\z@Bigrel#1{\z@rel{\zBig{#1}}}
  207. %
  208. \def\z@smallop#1{\z@op{\zsmall{#1}}}
  209. \def\z@smallbin#1{\z@bin{\zsmall{#1}}}
  210. \def\z@smallrel#1{\z@rel{\zsmall{#1}}}
  211. %
  212. % This underscore doesn't have the little kern --- you get an italic
  213. % correction anyway in math mode.
  214. \def\_{\leavevmode \vbox{\hrule width0.4em}}
  215.  
  216. % Save \q as \xq for quantifiers q.
  217. \let\xforall=\forall
  218. \let\xexists=\exists
  219. \let\xlambda=\lambda
  220. \let\xmu=\mu
  221. % Save other symbols
  222. \let\xsucc\succ
  223. \let\xprec\prec
  224. \let\dotaccent=\dot
  225. \let\sectionsymbol=\S
  226. \let\integral=\int
  227. \let\product\prod
  228.  
  229. % \p and \f make arrows with 1 and 2 crossings resp.
  230. \def\p#1{\mathrel{\ooalign{\hfil$\mapstochar\mkern 5mu$\hfil\cr$#1$}}}
  231. \def\f#1{\mathrel{\ooalign{\hfil
  232.     $\mapstochar\mkern 3mu\mapstochar\mkern 5mu$\hfil\cr$#1$}}}
  233. %
  234. %    ------ AMSTEX SYMBOL DEFINITIONS ------
  235. %
  236. % do these before Z symbols so that we can use them in our special symbols
  237. %
  238. %    msam font
  239. %
  240. \@mc \boxdot    "2\@fx00
  241. \@mc \boxplus    "2\@fx01
  242. \@mc \boxtimes    "2\@fx02
  243. \@mc \square      "0\@fx03
  244. \@mc \blacksquare    "0\@fx04
  245. \@mc \centerdot    "2\@fx05
  246. \@mc \lozenge    "0\@fx06
  247. \@mc \blacklozenge    "0\@fx07
  248. \@mc \circlearrowright    "3\@fx08
  249. \@mc \circlearrowleft    "3\@fx09
  250. \@mc \rightleftharpoons    "3\@fx0A
  251. \@mc \leftrightharpoons    "3\@fx0B
  252. \@mc \boxminus    "2\@fx0C
  253. \@mc \Vdash    "3\@fx0D
  254. \@mc \Vvdash    "3\@fx0E
  255. \@mc \vDash    "3\@fx0F
  256. \@mc \twoheadrightarrow    "3\@fx10
  257. \@mc \twoheadleftarrow    "3\@fx11
  258. \@mc \leftleftarrows    "3\@fx12
  259. \@mc \rightrightarrows    "3\@fx13
  260. \@mc \upuparrows    "3\@fx14
  261. \@mc \downdownarrows    "3\@fx15
  262. \@mc \upharpoonright    "3\@fx16
  263. \let \restriction    \upharpoonright
  264. \@mc \downharpoonright    "3\@fx17
  265. \@mc \upharpoonleft    "3\@fx18
  266. \@mc \downharpoonleft    "3\@fx19
  267. \@mc \rightarrowtail    "3\@fx1A
  268. \@mc \leftarrowtail    "3\@fx1B
  269. \@mc \leftrightarrows    "3\@fx1C
  270. \@mc \rightleftarrows    "3\@fx1D
  271. \@mc \Lsh    "3\@fx1E
  272. \@mc \Rsh    "3\@fx1F
  273. \@mc \rightsquigarrow    "3\@fx20
  274. \@mc \leftrightsquigarrow    "3\@fx21
  275. \@mc \looparrowleft    "3\@fx22
  276. \@mc \looparrowright    "3\@fx23
  277. \@mc \circeq    "3\@fx24
  278. \@mc \succsim    "3\@fx25
  279. \@mc \gtrsim    "3\@fx26
  280. \@mc \gtrapprox    "3\@fx27
  281. \@mc \multimap    "3\@fx28
  282. \@mc \therefore    "3\@fx29
  283. \@mc \because    "3\@fx2A
  284. \@mc \doteqdot    "3\@fx2B
  285. \let \Doteq    \doteqdot
  286. \@mc \triangleq    "3\@fx2C
  287. \@mc \precsim    "3\@fx2D
  288. \@mc \lesssim    "3\@fx2E
  289. \@mc \lessapprox    "3\@fx2F
  290. \@mc \eqslantless    "3\@fx30
  291. \@mc \eqslantgtr    "3\@fx31
  292. \@mc \curlyeqprec    "3\@fx32
  293. \@mc \curlyeqsucc    "3\@fx33
  294. \@mc \preccurlyeq    "3\@fx34
  295. \@mc \leqq    "3\@fx35
  296. \@mc \leqslant  "3\@fx36
  297. \@mc \lessgtr    "3\@fx37
  298. \@mc \backprime    "0\@fx38
  299. \@mc \risingdotseq    "3\@fx3A
  300. \@mc \fallingdotseq    "3\@fx3B
  301. \@mc \succcurlyeq    "3\@fx3C
  302. \@mc \geqq    "3\@fx3D
  303. \@mc \geqslant  "3\@fx3E
  304. \@mc \gtrless    "3\@fx3F
  305. \@mc \sqsubset    "3\@fx40
  306. \@mc \sqsupset    "3\@fx41
  307. \@mc \vartriangleright    "3\@fx42
  308. \@mc \vartriangleleft    "3\@fx43
  309. \@mc \trianglerighteq    "3\@fx44
  310. \@mc \trianglelefteq    "3\@fx45
  311. \@mc \bigstar    "0\@fx46
  312. \@mc \between    "3\@fx47
  313. \@mc \blacktriangledown    "0\@fx48
  314. \@mc \blacktriangleright    "3\@fx49
  315. \@mc \blacktriangleleft    "3\@fx4A
  316. \@mc \vartriangle    "0\@fx4D
  317. \@mc \blacktriangle    "0\@fx4E
  318. \@mc \triangledown    "0\@fx4F
  319. \@mc \eqcirc    "3\@fx50
  320. \@mc \lesseqgtr    "3\@fx51
  321. \@mc \gtreqless    "3\@fx52
  322. \@mc \lesseqqgtr    "3\@fx53
  323. \@mc \gtreqqless    "3\@fx54
  324. \def \yen    {\mathhexbox\@fx55 }
  325. \@mc \Rrightarrow    "3\@fx56
  326. \@mc \Lleftarrow    "3\@fx57
  327. \def \checkmark    {\mathhexbox\@fx58 }
  328. \@mc \veebar    "2\@fx59
  329. \@mc \barwedge    "2\@fx5A
  330. \@mc \doublebarwedge    "2\@fx5B
  331. \@mc \angle    "0\@fx5C
  332. \@mc \measuredangle    "0\@fx5D
  333. \@mc \sphericalangle    "0\@fx5E
  334. \@mc \varpropto    "3\@fx5F
  335. \@mc \smallsmile    "3\@fx60
  336. \@mc \smallfrown    "3\@fx61
  337. \@mc \Subset    "3\@fx62
  338. \@mc \Supset    "3\@fx63
  339. \@mc \Cup    "2\@fx64
  340. \let \doublecup    \Cup
  341. \@mc \Cap    "2\@fx65
  342. \let \doublecap    \Cap
  343. \@mc \curlywedge    "2\@fx66
  344. \@mc \curlyvee    "2\@fx67
  345. \@mc \leftthreetimes    "2\@fx68
  346. \@mc \rightthreetimes    "2\@fx69
  347. \@mc \subseteqq    "3\@fx6A
  348. \@mc \supseteqq    "3\@fx6B
  349. \@mc \bumpeq    "3\@fx6C
  350. \@mc \Bumpeq    "3\@fx6D
  351. \@mc \lll    "3\@fx6E
  352. \let \llless    \lll
  353. \@mc \ggg    "3\@fx6F
  354. \let \gggtr    \ggg
  355. \def \ulcorner    {\delimiter"4\@fx70\@fx70 }
  356. \def \urcorner    {\delimiter"5\@fx71\@fx71 }
  357. \def \circledR    {\mathhexbox\@fx72 }
  358. \@mc \circledS    "0\@fx73
  359. \@mc \pitchfork    "3\@fx74
  360. \@mc \dotplus    "2\@fx75
  361. \@mc \backsim    "3\@fx76
  362. \@mc \backsimeq    "3\@fx77
  363. \def \llcorner    {\delimiter"4\@fx78\@fx78 }
  364. \def \lrcorner    {\delimiter"5\@fx79\@fx79 }
  365. \def \maltese    {\mathhexbox\@fx7A }
  366. \@mc \complement    "0\@fx7B
  367. \@mc \intercal    "2\@fx7C
  368. \@mc \circledcirc    "2\@fx7D
  369. \@mc \circledast    "2\@fx7E
  370. \@mc \circleddash    "2\@fx7F
  371. %
  372. %    msbm font
  373. %
  374. \@mc \lvertneqq "3\@fy00
  375. \@mc \gvertneqq "3\@fy01
  376. \@mc \nleq    "3\@fy02
  377. \@mc \ngeq    "3\@fy03
  378. \@mc \nless    "3\@fy04
  379. \@mc \ngtr    "3\@fy05
  380. \@mc \nprec    "3\@fy06
  381. \@mc \nsucc    "3\@fy07
  382. \@mc \lneqq    "3\@fy08
  383. \@mc \gneqq    "3\@fy09
  384. \@mc \nleqslant    "3\@fy0A
  385. \@mc \ngeqslant    "3\@fy0B
  386. \@mc \lneq    "3\@fy0C
  387. \@mc \gneq    "3\@fy0D
  388. \@mc \npreceq    "3\@fy0E
  389. \@mc \nsucceq    "3\@fy0F
  390. \@mc \precnsim    "3\@fy10
  391. \@mc \succnsim    "3\@fy11
  392. \@mc \lnsim    "3\@fy12
  393. \@mc \gnsim    "3\@fy13
  394. \@mc \nleqq    "3\@fy14
  395. \@mc \ngeqq    "3\@fy15
  396. \@mc \precneqq    "3\@fy16
  397. \@mc \succneqq    "3\@fy17
  398. \@mc \precnapprox    "3\@fy18
  399. \@mc \succnapprox    "3\@fy19
  400. \@mc \lnapprox    "3\@fy1A
  401. \@mc \gnapprox    "3\@fy1B
  402. \@mc \nsim    "3\@fy1C
  403. \@mc \ncong    "3\@fy1D
  404. \def \napprox    {\not\approx}
  405. %\@mc \varsubsetneq "3\@fy20
  406. %\@mc \varsupsetneq "3\@fy21
  407. \@mc \nsubseteqq    "3\@fy22
  408. \@mc \nsupseteqq    "3\@fy23
  409. \@mc \subsetneqq    "3\@fy24
  410. \@mc \supsetneqq    "3\@fy25
  411. %\@mc \varsubsetneqq    "3\@fy26
  412. %\@mc \varsupsetneqq    "3\@fy27
  413. \@mc \subsetneq    "3\@fy28
  414. \@mc \supsetneq    "3\@fy29
  415. \@mc \nsubseteq    "3\@fy2A
  416. \@mc \nsupseteq    "3\@fy2B
  417. \@mc \nparallel    "3\@fy2C
  418. \@mc \nmid    "3\@fy2D
  419. \@mc \nshortmid    "3\@fy2E
  420. \@mc \nshortparallel    "3\@fy2F
  421. \@mc \nvdash    "3\@fy30
  422. \@mc \nVdash    "3\@fy31
  423. \@mc \nvDash    "3\@fy32
  424. \@mc \nVDash    "3\@fy33
  425. \@mc \ntrianglerighteq    "3\@fy34
  426. \@mc \ntrianglelefteq    "3\@fy35
  427. \@mc \ntriangleleft    "3\@fy36
  428. \@mc \ntriangleright    "3\@fy37
  429. \@mc \nleftarrow    "3\@fy38
  430. \@mc \nrightarrow    "3\@fy39
  431. \@mc \nLeftarrow    "3\@fy3A
  432. \@mc \nRightarrow    "3\@fy3B
  433. \@mc \nLeftrightarrow    "3\@fy3C
  434. \@mc \nleftrightarrow    "3\@fy3D
  435. \@mc \divideontimes    "2\@fy3E
  436. \@mc \varnothing    "0\@fy3F
  437. \@mc \mho    "0\@fy66
  438. \@mc \eth    "0\@fy67
  439. \@mc \eqsim    "3\@fy68
  440. \@mc \beth    "0\@fy69
  441. \@mc \gimel    "0\@fy6A
  442. \@mc \daleth    "0\@fy6B
  443. \@mc \lessdot    "3\@fy6C
  444. \@mc \gtrdot    "3\@fy6D
  445. \@mc \ltimes    "2\@fy6E
  446. \@mc \rtimes    "2\@fy6F
  447. \@mc \shortmid    "3\@fy70
  448. \@mc \shortparallel    "3\@fy71
  449. \def \interleave    {{\parallel\!\!\vert}}
  450. \def \shortinterleave    {\z@rel{\mathord\shortmid\mathord\shortparallel}}
  451. \@mc \smallsetminus    "2\@fy72
  452. \@mc \thicksim    "3\@fy73
  453. \@mc \thickapprox    "3\@fy74
  454. \@mc \approxeq    "3\@fy75
  455. \@mc \succapprox    "3\@fy76
  456. \@mc \precapprox    "3\@fy77
  457. \@mc \curvearrowleft    "3\@fy78
  458. \@mc \curvearrowright    "3\@fy79
  459. \@mc \digamma    "0\@fy7A
  460. \@mc \varkappa    "0\@fy7B
  461. \@mc \hslash    "0\@fy7D
  462. \@mc \hbar    "0\@fy7E
  463. \@mc \backepsilon    "3\@fy7F
  464. %
  465. %        ------ SPECIAL Z SYMBOLS ------
  466. %
  467. %    NUMBERS
  468. %
  469. \def \nat    {{\bbold N}}
  470. \def \integer    {{\bbold Z}}
  471. \def \natone    {{\bbold N}_1}
  472. \def \real    {{\bbold R}}
  473. \def \bool    {{\bbold B}}
  474. \let \divides    \div
  475. \def \div    {\z@bin{\rm div}}
  476. \def \mod    {\z@bin{\rm mod}}
  477. \def \succ    {\word{succ}}
  478. \def \expon    {^}
  479. %    aliases
  480. \let \num    \integer
  481. \let \nplus    \natone
  482. %
  483. %    LOGIC
  484. %
  485. \def \lnot    {\neg\;}
  486. \def \land    {\z@rel{\wedge}}
  487. \def \lor    {\z@rel{\vee}}
  488. \let \imp    \Rightarrow
  489. \let \iff    \Leftrightarrow
  490. \def \all    {\z@op{\xforall}}
  491. \def \exi    {\z@op{\xexists}}
  492. \def \exione    {\exists_1}
  493. \@mc \nexi    "0\@fy40
  494. \def \dot    {\z@rel{\bullet}}
  495. \def \true    {\keyword{true}}
  496. \def \false    {\keyword{false}}
  497. \let \cond    \rightarrow
  498. %    aliases
  499. \let \spot    \dot
  500. \mathcode`\@="8000% make @ active in mathmode
  501. {\catcode`\@=\active \gdef@{\dot}}
  502. \let \implies    \imp
  503. \let \forall    \all
  504. \let \exists    \exi
  505. \let \nexists    \nexi
  506. %
  507. %    SETS
  508. %
  509. \let \emptyset  \varnothing
  510. \def \varemptyset  {\{\,\}}
  511. \def \pset    {\z@op{\bbold P}}
  512. \def \psetone    {\pset_1}
  513. \def \fset    {\z@op{\bbold F}}
  514. \def \fsetone    {\fset_1}
  515. \def \sset    {\z@op{\bbold S}}
  516. \let \mem    \in
  517. \def \nem    {\not\mem}
  518. \def \uni    {\z@bin\cup}
  519. \def \int    {\z@bin\cap}
  520. \let \prod    \times
  521. \def \min    {\word{min}}
  522. \def \max    {\word{max}}
  523. \def \duni    {\z@Bigop{\lower0.25ex\hbox{$\uni$}}}
  524. \def \dint    {\z@Bigop{\lower0.25ex\hbox{$\int$}}}
  525. \def \upto    {\z@bin{\ldotp\ldotp}}
  526. \let \psubs    \subset
  527. \let \subs    \subseteq
  528. \let \psups    \supset
  529. \let \sups    \supseteq
  530. \def \diff    {\z@bin{\backslash}}
  531. %    aliases
  532. \let \cross    \prod
  533. \let \notin    \nem
  534. \let \nmem    \nem
  535. \let \union    \uni
  536. \let \inter    \int
  537. \let \power    \pset
  538. \let \finset    \fset
  539. \let \dunion    \duni
  540. \let \dinter    \dint
  541. %
  542. %    RELATIONS & FUNCTIONS
  543. %
  544. \def \lambda    {\z@op{\xlambda}}
  545. \def \mu    {\z@op{\xmu}}
  546. \def \dom    {\keyword{dom}}
  547. \def \ran    {\keyword{ran}}
  548. \def \id    {\keyword{id}}
  549. \@mc \dres    "2\@fx43
  550. \@mc \rres    "2\@fx42
  551. \def \dsub    {\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\dres}}}
  552. \def \rsub    {\mathbin{\rlap{\raise.05ex\hbox{$-$}}{\rres}}}
  553. \let \fovr    \oplus
  554. \let \cmp    \circ
  555. \def \fcmp    {\mathbin{\raise 0.6ex\hbox{\oalign{\hfil$\scriptscriptstyle
  556.          \rm o$\hfil\cr\hfil$\scriptscriptstyle\rm 9$\hfil}}}}
  557. \def \inv    {^\sim}
  558. \def \limg    {(\!|}
  559. \def \rimg    {|\!)}
  560. \let \map    \mapsto
  561. \let \rel    \leftrightarrow
  562. \let \tfun    \rightarrow
  563. \let \tinj    \rightarrowtail
  564. \def \tsur    {\mathrel{\ooalign{$\tfun$\hfil\cr$\mkern4mu\tfun$}}}
  565. \def \pfun    {\p\tfun}
  566. \def \pinj    {\p\tinj}
  567. \def \psur    {\p\tsur}
  568. \def \ffun    {\f\tfun}
  569. \def \finj    {\f\tinj}
  570. \def \bij    {\mathrel{\ooalign{$\tinj$\hfil\cr$\mkern5mu\tfun$}}}
  571. \def \tcl    {^+}
  572. \def \rtcl    {^*}
  573. \def \iter    {^}
  574. %    aliases
  575. \let \comp    \fcmp
  576. \let \ndres    \dsub
  577. \let \nrres    \rsub
  578. \let \fun    \tfun
  579. \let \inj    \tinj
  580. \let \surj    \tsur
  581. \let \psurj    \psur
  582. %
  583. %    SEQUENCES
  584. %
  585. \def \seq    {\keyword{seq}}
  586. \def \iseq    {\keyword{iseq}}
  587. \def \seqone    {\seq_1}
  588. \def \emptyseq  {\lseq\,\rseq}
  589. \let \lseq    \langle
  590. \let \rseq    \rangle
  591. \def \head    {\word{head}}
  592. \def \tail    {\word{tail}}
  593. \def \front    {\word{front}}
  594. \def \last    {\word{last}}
  595. \def \rev    {\word{rev}}
  596. \def \squash    {\word{squash}}
  597. \def \next    {\keyword{next}}
  598. \def \inseq    {\keyword{in}}
  599. \def \cat    {\mathbin{\raise 0.8ex\hbox{$\mathchar"2\@fx61$}}}
  600. \@mc \sres    "2\@fx16
  601. \def \ssub    {\z@bin{\rlap{$-$}{\sres}}}
  602. \@mc \ires    "2\@fx18
  603. \def \isub    {\z@bin{\rlap{$-$}{\ires}}}
  604. \def \dcat    {\z@op{\cat/}}
  605. \def \dovr    {\z@op{\fovr/}}
  606. \def \dcmp    {\z@op{\fcmp/}}
  607. \let \prefix    \subseteq
  608. \def \suffix    {\keyword{suffix}}
  609. \def \seqi    {\keyword{seq_\infty}}
  610. \def \partitions    {\keyword{partitions}}
  611. \def \partition    {\keyword{partitions}}
  612. \def \disjoint    {\keyword{disjoint}}
  613. \def \subseq    {\keyword{subseq}}
  614. %    aliases
  615. \let \filter    \sres
  616. %
  617. %    SCHEMAS
  618. %
  619. \def \lsch    {\z@bigop{\hbox{[}}}
  620. \def \rsch    {\z@bigop{\hbox{]}}}
  621. \def \dparallel    {\z@bigop{\parallel}\limits}
  622. \def \zand    {\z@bigbin\land}
  623. \def \zor    {\z@bigbin\lor}
  624. \def \zcmp    {\z@bigbin\fcmp}
  625. \def \zexi    {\z@bigop\exists}
  626. \def \zall    {\z@bigop\forall}
  627. \def \znot    {\z@bigop\neg}
  628. \def \zbar    {\z@bigbin\cbar}
  629. \def \zfor    {/}
  630. \def \zhide    {\z@bigbin\backslash}
  631. \def \zimp    {\z@bigrel\imp}
  632. \def \zeq    {\z@bigrel\iff}
  633. \def \zovr    {\z@bigrel\oplus}
  634. \def \zpipe    {\z@bigbin{\mathord>\!\!\mathord>}}
  635. \def \pre    {\keyword{pre}}
  636. \def \pred    {\keyword{pred}}
  637. \def \post    {\keyword{post}}
  638. \def \zproject    {\z@bigbin\sres}
  639. \def\rename{\@ifnextchar*{\z@rename}{\z@@rename}}
  640. \def\z@rename*[#1/#2]{\left[#1 \over #2\right]}
  641. \def\z@@rename[#1/#2]{\left[#1 \zfor #2\right]}
  642. %    aliases
  643. \let \project    \zproject
  644. \let \import    \sres
  645. \let \semi    \zcmp
  646. \let \hide    \zhide
  647. %
  648. %    BAGS
  649. %
  650. \let\buni\uplus
  651. \def \emptybag  {\lbag\:\rbag}
  652. \def \lbag    {[\![}
  653. \def \rbag    {]\!]}
  654. \def \bag    {\keyword{bag}}
  655. \def \items    {\word{items}}
  656. \let \inbag    \inseq
  657. \def \bagcount    {\word{count}}
  658. %
  659. %    DEFINITIONS & DECLARATIONS
  660. %
  661. \def \ddef    {\z@rel{\;::=\;}}
  662. \def \bbar    {\z@bigrel\mid}
  663. \let \cbar    \mid
  664. \def \lang    {\langle\!\langle}
  665. \def \rang    {\rangle\!\rangle}
  666. \def \sdef    {\z@rel{\widehat=}}
  667. \def \defs    {\z@smallrel{==}}
  668. \def \varsdef    {\z@rel\triangleq}
  669. %    aliases
  670. \let \sdefs    \sdef
  671. \mathcode`\|=\mid
  672. \let \ldata    \lang
  673. \let \rdata    \rang
  674. %
  675. %    MISCELLANEOUS
  676. %
  677. \def \lblot     {\langle\!|}
  678. \def \rblot     {|\!\rangle}
  679. \def \IMP    {\boldword{Import}}
  680. \let \env    \Rrightarrow
  681. \def \zlet      {\boldword{let}}
  682. \def \zin       {\boldword{in}}
  683. \def \zwhere    {\boldword{where}}
  684. %
  685. %    QZED SUPPORT
  686. %
  687. \def\HOLE{\z@op{\hbox{$\lll\star\star\star\ggg$}}}
  688. \def\landd{} % to support qzed editor
  689. \def\semid{} % to support qzed editor
  690. \def\qzed{\ifz@inclass\else\zed\fi}
  691. \def\endqzed{\ifz@inclass\else\endzed\fi}
  692. %
  693. %    CLASSES
  694. %
  695. \def\qua{\mbox{::}}
  696. \def\redef{\mbox{\bf ~redef}}
  697. \def\Init{I\!{\scriptstyle NIT}}
  698. \def\Exit{E\!{\scriptstyle XIT}}
  699. \def\Internal{I\!{\scriptstyle NTERNAL}}
  700. \def\Aux{A\!{\scriptstyle UX}}
  701. \def\intern{\mbox{\sf i}}
  702. %
  703. %        ------ OTHER SPECIAL NOTATION ------
  704. %
  705. %    PROOFS
  706. %
  707. \def\thrm{\z@rel\vdash}
  708. \def\qed{\zsmall\Box}
  709. \let\Qed\Box
  710. \let\QED\square
  711. \def\BLACKQED{\zsmall\blacksquare}
  712. \let\ETH\qed
  713. \def\TH{\boldword{Theorem}}
  714. \def\LE{\boldword{Lemma}}
  715. \def\PR{\boldword{Proof}}
  716. \def\refines{\z@rel\sqsupseteq}
  717. \def\defines{\z@rel\sqsubseteq}
  718. \def\weakrefine{\z@rel{\raise0.2ex\rlap{\hbox{$\sqsupset$}}\lower1ex\hbox{$\sim$}}}
  719. \def\weakdefine{\z@rel{\raise0.2ex\rlap{\hbox{$\sqsubset$}}\lower1ex\hbox{$\sim$}}}
  720. %    aliases
  721. \let\shows\thrm
  722. %
  723. %    OBJECT THEORY
  724. %
  725. \def\childof{\z@rel\xsucc}
  726. \def\parentof{\z@rel\xprec}
  727. \let\weaksubclass\succsim
  728. \let\weaksupclass\precsim
  729. \def\hasa{\z@rel{\mathord\xsucc\!\!\!\mathord\xsucc}}
  730. \def\instancein{\z@rel{\mathord\xprec\!\!\!\mathord\xprec}}
  731. \def\subtype{\z@rel\sqsubset}
  732. \def\subtypeeq{\z@rel\sqsubseteq}
  733. \def\suptype{\z@rel\sqsupset}
  734. \def\suptypeeq{\z@rel\sqsupseteq}
  735. %    aliases
  736. \let\inherits\childof
  737. \let\subclass\childof
  738. \let\isa\childof
  739. \let\supclass\parentof
  740. \let\instantiates\hasa
  741. \let\islikea\weaksubclass
  742. \def\poly{\mathord\downarrow}
  743. %WAS: \def\widen{\z@op\downarrow}
  744. \def\widen#1{\z@op{{\overline{#1}}}}
  745. %
  746. %    TEMPORAL LOGIC
  747. %
  748. \def\atnext{\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\zSmall\bigcirc$}\kern0.01em\zSmall\bigcirc}
  749. \def\atlast{\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\zSmall\bigcirc$}\kern0.01em\rlap{$\kern0.01em\mathord-$}\zSmall\bigcirc}
  750. \def\always{\lower0.37ex\hbox{$\zbig\Box$}}
  751. \def\uptilnow{\rlap{$\kern0.02em\mathord-$}\lower0.37ex\hbox{$\zbig\Box$}}
  752. \def\eventually{\lower0.37ex\hbox{$\zbig\Diamond$}}
  753. \def\previously{\rlap{$\kern0.04em\mathord-$}\lower0.37ex\hbox{$\zbig\Diamond$}}
  754. %    aliases
  755. \let\henceforth\always
  756. %
  757. %    ORDERS
  758. %
  759. \def \mono    {\keyword{monotonic}}
  760. \def \porder    {\keyword{partial\_order}}
  761. \def \torder    {\keyword{total\_order}}
  762. %
  763. %    WORD STYLES
  764. %
  765. \def\String#1{\hbox{`{\tt #1}'}}
  766. \def\STRING#1{\hbox{``{\tt #1}''}}
  767. \def\infix#1{\z@rel{{\underline{#1}}}}
  768. \def\word#1{\z@op{#1}}
  769. \def\keyword#1{\z@op{\rm #1}}
  770. \def\boldword#1{\z@op{\bf #1}}
  771. \def\underword#1{\z@op{{\underline{#1}}}}
  772. \def\underkeyword#1{\z@op{{\underline{\rm #1}}}}
  773. \def\underboldword#1{\z@op{{\underline{\bf #1}}}}
  774. \newbox\z@combox\newdimen\z@wdcalc
  775. \def\comment{\@ifnextchar*{\z@leftcomment}{\z@comment}}
  776. \def\z@comment#1{$\z@stopfield\z@addfield\z@startfield$\global\setbox\z@combox\hbox{\quad[{\sf #1}]}\z@wdcalc=\wd\z@combox\advance\z@wdcalc by \wd\z@curline\advance\z@wdcalc by \z@curindent\advance\z@wdcalc by \zedleftsep\advance\z@wdcalc by \zedlinethickness\advance\z@wdcalc by 2\zedindent\ifdim\z@wdcalc>\displaywidth\\\fi&\box\z@combox\ignorespaces}
  777. \def\z@leftcomment*#1{\hbox{[{\sf #1}]}}
  778. %
  779. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  780. %
  781. %    SECTION 3    Z ENVIRONMENTS
  782. %
  783. %        ------ MARGIN STACK ------
  784. %
  785. % define a stack of dimensions (50 elements)
  786. %    can probably be made smaller when qzed filters its TeX output better
  787. \newcount\z@stackmin
  788. \newcount\z@stackmax
  789. \newcount\z@stacktop
  790. \newdimen\@gtempa \z@stackmin=\allocationnumber
  791. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  792. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  793. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  794. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  795. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  796. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  797. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  798. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  799. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  800. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  801. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  802. \newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa\newdimen\@gtempa
  803. \newdimen\@getempa \z@stackmax=\allocationnumber
  804. \dimen\z@stackmin=0pt
  805.  
  806. % define a box to contain the current line
  807. %  & a variable to contain it's indentation
  808. \newbox\z@curline
  809. \newdimen\z@curindent
  810. \dimen\z@curindent=0pt
  811. % Space between operands of a function application
  812. \def\z@space{{}\;{}}
  813.  
  814. % define a box to contain the current field
  815. \newbox\z@curfield
  816.  
  817. % define a mini-tabbing environment for use inside 'zed'
  818. \def\z@startline{\setbox\z@curline\hbox{}%
  819.                  \global\z@curindent\dimen\z@stacktop
  820.                  \z@startfield\ignorespaces}
  821. \def\z@stopline{\z@stopfield
  822.                 \z@addfield
  823.                 \hbox{\hskip\z@curindent \box\z@curline}}
  824.  
  825. \def\z@startfield{\global\setbox\z@curfield\hbox\bgroup}
  826. \def\z@stopfield{\egroup}
  827. \def\z@addfield{\global\setbox\z@curline\hbox{\unhbox
  828.                  \z@curline\unhbox\z@curfield}}
  829.  
  830. \def\z@pushmargin{\hbox{\kern0pt}$%
  831.                   \z@stopfield
  832.                   \z@addfield
  833.                   \ifnum \z@stacktop < \z@stackmax
  834.                     \global\advance\z@stacktop \@ne
  835.                   \else
  836.                     \@latexerr{Z margin stack overflow (too many \string\M's)}
  837.             \@ehd
  838.                   \fi
  839.                   \global\dimen\z@stacktop\z@curindent
  840.                   \global\advance\dimen\z@stacktop \wd\z@curline
  841.                   \z@startfield\ignorespaces
  842.                   $\relax}
  843. \def\z@popmargin{\ifnum \z@stacktop > \z@stackmin
  844.                     \global\advance\z@stacktop \m@ne \ignorespaces
  845.                   \else
  846.                     \@latexerr{Z Margin stack underflow (too many \string\O's)}
  847.             \@ehd
  848.                   \fi}
  849. \def\M{\z@pushmargin} \def\O{\z@popmargin} \def\S{\z@space}
  850. \z@stacktop\z@stackmin
  851. %
  852. %        ------ UTILITY MACROS FOR Z ENVIRONMENTS ------
  853. %
  854. % Here are environments for the various sorts of displays which occur in
  855. % Z documents. All displays are set flush left, indented by \zedindent,
  856. % by default \leftmargini.  Schemas, etc, are made just wide enough to
  857. % give equal margins left and right.
  858. %
  859. % Some environments (schema, etc.) must only be split at `\zbreak',
  860. % and others (e.g. argue) may be split arbitrarily. All generate
  861. % alignment displays, and penalties are used to control page breaks.
  862. %
  863. %    FORMAT and CONTROL macros
  864. %
  865. \newdimen\zedindent        \zedindent=\leftmargini
  866. \newdimen\zedleftsep        \zedleftsep=1em
  867. \newdimen\zedtab        \zedtab=2em
  868. \newdimen\zedbar        \zedbar=8em
  869. \newdimen\zedlinethickness    \zedlinethickness=0.4pt
  870. \newdimen\zedcornerheight    \zedcornerheight=0pt
  871. \newcount\z@cols
  872. %
  873. \newif\ifz@firstline        \z@firstlinefalse
  874. \newif\ifz@inclass        \z@inclassfalse
  875. \newif\ifz@inenv        \z@inenvfalse
  876. \newif\ifz@leftmargin        \z@leftmargintrue
  877. \newif\ifz@incols        \z@incolsfalse
  878. \newif\ifleftnames        \leftnamesfalse
  879. \def\leftschemas{\leftnamestrue}
  880. \newif\ifz@inbox        \z@inboxfalse
  881. %
  882. \newskip\zedbaselineskip    \zedbaselineskip\baselineskip
  883. \newbox\zstrutbox        \setbox\zstrutbox=\copy\strutbox
  884. \def\zstrut{\relax\ifmmode\copy\zstrutbox\else\unhcopy\zstrutbox\fi}
  885. \def\zedbaselinestretch{1}
  886. %
  887. % penalties
  888. %
  889. \newcount\interzedlinepenalty    \interzedlinepenalty=10000    %never break
  890. \newcount\preboxpenalty        \preboxpenalty=0        %break easily
  891. \newcount\forcepagepenalty    \forcepagepenalty=-10000    %always break
  892. % also use            \interdisplaylinepenalty=100    %break sometimes
  893. %
  894. % macros for changing the size of schema text
  895. %
  896. \def\zedsize#1{\def\z@size{#1}}
  897. \def\z@size{}
  898. \newskip\z@adskip\newskip\z@bdskip\newskip\z@adsskip\newskip\z@bdsskip
  899. \def\z@changesize{%
  900. \z@adskip\abovedisplayskip\z@bdskip\belowdisplayskip% save skips
  901. \z@adsskip\abovedisplayshortskip\z@bdsskip\belowdisplayshortskip
  902. \z@size % change size
  903. \abovedisplayskip\z@adskip\belowdisplayskip\z@bdskip% restore skips
  904. \abovedisplayshortskip\z@adsskip\belowdisplayshortskip\z@bdsskip}
  905. %
  906. \def\zBIG#1{\hbox{\ifx\z@ptsize \vpt \viiipt\@viiipt
  907.     \else \ifx\z@ptsize \vipt \ixpt\@ixpt
  908.     \else \ifx\z@ptsize \viipt \xpt\@xpt
  909.     \else \ifx\z@ptsize \viiipt \xipt\@xipt
  910.     \else \ifx\z@ptsize \ixpt \xiipt\@xiipt
  911.     \else \ifx\z@ptsize \xpt \xivpt\@xivpt
  912.     \else \ifx\z@ptsize \xipt \xviipt\@xviipt
  913.     \else \ifx\z@ptsize \xiipt \xxpt\@xxpt
  914.     \else \ifx\z@ptsize \xivpt \xxvpt\@xxvpt
  915.     \else \ifx\z@ptsize \xviipt \xxvpt\@xxvpt
  916.     \else \ifx\z@ptsize \xxpt \xxvpt\@xxvpt
  917.     \else \@warning{Can't increase this font size}
  918.     \fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi $\mathord{#1}$}}
  919. \def\zBig#1{\hbox{\ifx\z@ptsize \vpt \viipt\@viipt
  920.     \else \ifx\z@ptsize \vipt \viiipt\@viiipt
  921.     \else \ifx\z@ptsize \viipt \ixpt\@ixpt
  922.     \else \ifx\z@ptsize \viiipt \xpt\@xpt
  923.     \else \ifx\z@ptsize \ixpt \xipt\@xipt
  924.     \else \ifx\z@ptsize \xpt \xiipt\@xiipt
  925.     \else \ifx\z@ptsize \xipt \xivpt\@xivpt
  926.     \else \ifx\z@ptsize \xiipt \xviipt\@xviipt
  927.     \else \ifx\z@ptsize \xivpt \xxpt\@xxpt
  928.     \else \ifx\z@ptsize \xviipt \xxvpt\@xxvpt
  929.     \else \ifx\z@ptsize \xxpt \xxvpt\@xxvpt
  930.     \else \@warning{Can't increase this font size}
  931.     \fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi $\mathord{#1}$}}
  932. \def\zbig#1{\hbox{\ifx\z@ptsize \vpt \vipt\@vipt
  933.     \else \ifx\z@ptsize \vipt \viipt\@viipt
  934.     \else \ifx\z@ptsize \viipt \viiipt\@viiipt
  935.     \else \ifx\z@ptsize \viiipt \ixpt\@ixpt
  936.     \else \ifx\z@ptsize \ixpt \xpt\@xpt
  937.     \else \ifx\z@ptsize \xpt \xipt\@xipt
  938.     \else \ifx\z@ptsize \xipt \xiipt\@xiipt
  939.     \else \ifx\z@ptsize \xiipt \xivpt\@xivpt
  940.     \else \ifx\z@ptsize \xivpt \xviipt\@xviipt
  941.     \else \ifx\z@ptsize \xviipt \xxpt\@xxpt
  942.     \else \ifx\z@ptsize \xxpt \xxvpt\@xxvpt
  943.     \else \@warning{Can't increase this font size}
  944.     \fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi $\mathord{#1}$}}
  945. \def\zsmall#1{\hbox{\ifx\z@ptsize \vipt \vpt\@vpt
  946.     \else \ifx\z@ptsize \viipt \vipt\@vipt
  947.     \else \ifx\z@ptsize \viiipt \viipt\@viipt
  948.     \else \ifx\z@ptsize \ixpt \viiipt\@viiipt
  949.     \else \ifx\z@ptsize \xpt \ixpt\@ixpt
  950.     \else \ifx\z@ptsize \xipt \xpt\@xpt
  951.     \else \ifx\z@ptsize \xiipt \xipt\@xipt
  952.     \else \ifx\z@ptsize \xivpt \xiipt\@xiipt
  953.     \else \ifx\z@ptsize \xviipt \xivpt\@xivpt
  954.     \else \ifx\z@ptsize \xxpt \xviipt\@xviipt
  955.     \else \ifx\z@ptsize \xxvpt \xxpt\@xxpt
  956.     \else \@warning{Can't decrease this font size}
  957.     \fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi $\mathord{#1}$}}
  958. \def\zSmall#1{\hbox{\ifx\z@ptsize \vipt \vpt\@vpt
  959.     \else \ifx\z@ptsize \viipt \vpt\@vpt
  960.     \else \ifx\z@ptsize \viiipt \vipt\@vipt
  961.     \else \ifx\z@ptsize \ixpt \viipt\@viipt
  962.     \else \ifx\z@ptsize \xpt \viiipt\@viiipt
  963.     \else \ifx\z@ptsize \xipt \ixpt\@ixpt
  964.     \else \ifx\z@ptsize \xiipt \xpt\@xpt
  965.     \else \ifx\z@ptsize \xivpt \xipt\@xipt
  966.     \else \ifx\z@ptsize \xviipt \xiipt\@xiipt
  967.     \else \ifx\z@ptsize \xxpt \xivpt\@xivpt
  968.     \else \ifx\z@ptsize \xxvpt \xviipt\@xviipt
  969.     \else \@warning{Can't decrease this font size}
  970.     \fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi $\mathord{#1}$}}
  971. %
  972. \def\z@zeroskips{\abovedisplayskip\z@\belowdisplayskip\z@
  973.     \abovedisplayshortskip\z@\belowdisplayshortskip\z@}
  974. %
  975. %    Make zedbaselinestretch have an automatic effect
  976. %        adapted from lfonts.tex
  977. %
  978. \def\@setsize#1#2#3#4{\@nomath#1\let\@currsize#1\baselineskip
  979.     #2\baselineskip\baselinestretch\baselineskip
  980.     \setbox\strutbox\hbox{\vrule height.7\baselineskip
  981.     depth.3\baselineskip width\z@}\normalbaselineskip
  982.     \baselineskip #3#4\zedbaselineskip
  983.     #2\zedbaselineskip\zedbaselinestretch\zedbaselineskip
  984.     \setbox\zstrutbox\hbox{\vrule height.7\zedbaselineskip
  985.     depth.3\zedbaselineskip width\z@}\let\z@ptsize#3}
  986. %
  987. %        ------ MACROS FOR MARGINS ------
  988. %
  989. % \z@narrow, \z@wide - make the margins narrower, wider
  990. %
  991. \def\z@narrow{\advance\linewidth by -\zedindent}
  992. \def\z@wide{\advance\linewidth by \zedindent}
  993. %
  994. %        ------ MACROS FOR DRAWING BOXES ------
  995. %
  996. % \z@hrulefill - line with correct thickness
  997. %
  998. \def\z@hrulefill{\leaders\hrule height\zedlinethickness\hfill}
  999. %
  1000. % \z@topline draws the top horizontal line of boxed environments
  1001. % \z@dbltopline draws a double ruled top line
  1002. % \z@botline draws the bottom horizontal line of boxed environments
  1003. % \zedline[comment] draws a long horizontal line ending in comment
  1004. % \where draws a short horizontal line
  1005. %
  1006. \def\z@topline#1{\omit\@ifnextchar[{\z@@topline{#1}}{\z@@topline{#1}[]}}
  1007. \def\z@@topline#1[#2]{\hbox to\linewidth{\zstrut\ifleftnames\else
  1008.     \vrule height\zedlinethickness width\zedlinethickness
  1009.     \hbox to\zedleftsep{\z@hrulefill}\fi#1\z@hrulefill
  1010.     \smash{\vrule height\zedlinethickness width\zedlinethickness
  1011.     depth\zedcornerheight}\hbox{\sf #2}}\cr}
  1012. \def\z@dbltopline#1{\omit\@ifnextchar[{\z@@dbltopline{#1}}{\z@@dbltopline{#1}[]}}
  1013. \def\z@@dbltopline#1[#2]{\z@@topline{#1}[#2]%
  1014. \noalign{\kern-\baselineskip
  1015.     \kern-\zedlinethickness
  1016.     \kern-\doublerulesep \nobreak}%
  1017. \omit\z@@topline{\hphantom{#1}}[\hphantom{#2}]%
  1018. \noalign{\kern\doublerulesep
  1019.     \kern\zedlinethickness \nobreak}}
  1020. \def\z@botline{\also\omit\hbox to\linewidth{\z@hrulefill
  1021. \smash{\vrule height\zedcornerheight width\zedlinethickness
  1022.         depth 0pt}}\cr}
  1023. \def\z@@botline[#1]{\hbox to\linewidth{\vrule\z@hrulefill\hbox{\sf\smash{#1}}}\also}
  1024. \def\zedline{\also\omit\@ifnextchar[{\z@@botline}{\z@@botline[]}}
  1025. \def\where{\also \omit \hbox to\zedbar{\z@hrulefill}\cr\also}
  1026. \let \ST    \where
  1027. %
  1028. % \z@left is placed at the left of each z line:
  1029. %    in non-box environments it will do nothing.
  1030. %    in boxed environments it will do a vertical line with the same
  1031. %        height as the maximum height of the line.
  1032. %
  1033. \def\z@left{\ifz@inbox\vrule width\zedlinethickness\hskip\zedleftsep\fi}
  1034. %
  1035. %        ------ MACROS FOR SETTING UP Z ENVIRONMENTS ------
  1036. %
  1037. \def\z@env{\global\z@firstlinetrue\z@changesize
  1038.     $$\z@inenvtrue\baselineskip\zedbaselineskip
  1039.     \parskip=0pt\lineskip=0pt\z@narrow
  1040.     \advance\displayindent by \zedindent
  1041.         \def\\{\crcr}% Must have \def and not \let for nested alignments.
  1042.         \everycr={\noalign{\ifz@firstline \global\z@firstlinefalse
  1043.                 \else \penalty\interzedlinepenalty \fi}}
  1044.         \tabskip=0pt}
  1045. \def\endz@env{$$\global\@ignoretrue}
  1046. %
  1047. % z lines are formated in two (overlaping) columns;
  1048. %    the first flush left having the same width as the environment,
  1049. %    and, the second flush right ending at the right end of the environment.
  1050. %
  1051. \def\z@format{\halign to\linewidth\bgroup%
  1052.         \zstrut\z@left\z@startline\ignorespaces$\@lign##$\z@stopline\hfil%
  1053.         \tabskip=0pt plus1fil%
  1054.         &\hbox to 0pt{\hss\@lign##}\tabskip=0pt\cr}
  1055. %
  1056. \def\z@boxenv{\z@narrow\let\also=\als@ \let\Also=\Als@ \let\ALSO=\ALS@
  1057.     \z@inboxtrue \predisplaypenalty=\preboxpenalty \z@env\z@format}
  1058. %
  1059. \def\z@outnonbox{\z@outclasscheck\z@leavevmode\z@env}
  1060. \def\z@inoutbox{\z@leavevmode\z@makeouter\z@inclassfalse\z@boxenv}
  1061. %
  1062. %    SPACING COMMANDS
  1063. %
  1064. % no vertical glue between abutted lines
  1065. %
  1066. \def\@but{\noalign{\nointerlineskip}}
  1067. %
  1068. % no \par extra vertical spacing after Z environments
  1069. %
  1070. %\def\z@nopar{\ifz@inclass\else\vskip-\parskip\fi}
  1071. %\def\z@nopar{\global\parskip0pt\global\everypar{\parskip30mm\everypar{}}}
  1072. \def\z@nopar{\global\@endpetrue}
  1073. %
  1074. % \z@leavevmode -- Enter horizontal mode, taking account of possible
  1075. % interaction with lists and section heads:
  1076. %
  1077. %    1    After a \item, use \indent to get the label (this
  1078. %        fails to run in even short labels).
  1079. %    2    After a run-in heading, use \indent.
  1080. %    3    After an ordinary heading, throw away the \everypar
  1081. %        tokens, reset \@nobreak, and use \noindent with \parskip
  1082. %        zero.
  1083. %    4    Otherwise, use \noindent with \parskip zero
  1084. %
  1085. % use when entering displayed environments to get correct spacing
  1086. %
  1087. \def\z@leavevmode{\ifvmode\if@inlabel\indent\else\if@noskipsec\indent\else
  1088.     \if@nobreak\global\@nobreakfalse\everypar={}\fi
  1089.     {\parskip=0pt\noindent}\fi\fi\fi}
  1090. %
  1091. % extra vertical space in non-box environments
  1092. %
  1093. \def\also{\crcr\noalign{\vskip\jot}}
  1094. \def\Also{\crcr\noalign{\vskip2\jot}}
  1095. \def\ALSO{\Also\Also}
  1096. %
  1097. % extra vertical space in boxed environments
  1098. %
  1099. \def\als@{\crcr\@but\omit\vrule height\jot width\zedlinethickness \cr \@but}
  1100. \def\Als@{\crcr\@but\omit\vrule height2\jot width\zedlinethickness \cr \@but}
  1101. \def\ALS@{\crcr\@but\omit\vrule height4\jot width\zedlinethickness \cr \@but}
  1102. %
  1103. %    ENVIRONMENT-BREAKING COMMANDS
  1104. %
  1105. \def\znewpage{\also\noalign{\penalty\forcepagepenalty}\also}
  1106. \def\zbreak{\also\noalign{\penalty\interdisplaylinepenalty\vskip-\jot}\also}
  1107. \def\Zbreak{\also\noalign{\penalty\interdisplaylinepenalty}\also}
  1108. \def\ZBREAK{\Also\noalign{\penalty\interdisplaylinepenalty}\Also}
  1109. %
  1110. \def\t#1{\hskip #1\zedtab}
  1111. \def\c#1#2{\hbox to #1\zedtab{$#2$\hfil}}
  1112. \def\flushr#1{\crcr\quad\cr}
  1113. %
  1114. %        ------ UTILITY MACROS FOR OBJECT-Z ------
  1115. %
  1116. \def\z@inclasscheck{\ifz@inclass\else
  1117.     \@latexerr{This Z environment is only allowed within a class}
  1118. {Perhaps you forgot to include a \string\begin\string{class\string}
  1119. somewhere^^Jor you are trying to print a file that needs updating.^^J\@ehc} \fi}
  1120. \def\z@outclasscheck{\ifz@inclass
  1121.     \@latexerr{This Z environment is not allowed inside a class}
  1122. {This environment doesn't really make sense within a class.^^J%
  1123. If you really want it then I'll try my best to fit in in.^^J\@ehc}\else
  1124. \ifz@inenv \@latexerr{New Z environment declared before previous
  1125. one is completed}
  1126. {I suspect that you've forgotten to finish the last environment.^^J%
  1127. You are trying to nest environments and this can only be done inside classes^^J%
  1128. besides, the environment you have started isn't valid within classes any way.^^JI suggest that you type \space X <return> \space to quit and then correct your document.}
  1129. \fi\fi}
  1130. %
  1131. \def\z@makeouter{\ifz@inenv\ifz@inclass\z@inenvfalse
  1132.     \hskip-\zedleftsep \advance\linewidth by -\zedlinethickness
  1133.     \zedindent=\zedleftsep \zedleftsep=0.8\zedleftsep
  1134.     \zedbar=0.8\zedbar \zedtab=0.8\zedtab
  1135.     \parbox[b]{\linewidth}\bgroup\z@zeroskips
  1136.     \else\@latexerr{Incorrect place for Z environment; nesting is
  1137. allowed only inside classes}
  1138. {You've either forgotten to finish the last environment,^^J%
  1139. you've forgotten to include a \string\begin\string{class\string} somewhere^^J%
  1140. or you are trying to print a file that needs updating.^^J%
  1141. (Then again, you might just be trying to do something^^J%
  1142. that the author of these macros didn't intend you to do)^^J\@ehc}
  1143.     \fi\else\bgroup\fi}
  1144. %
  1145. \def \z@makeinner{\egroup%
  1146. \global\z@curindent\z@}
  1147. %
  1148. \def \classbreak{\also\egroup$$\vskip -\ht\zstrutbox
  1149.     \vskip -\abovedisplayskip\vskip -\belowdisplayskip\z@wide\z@boxenv\also}
  1150. %
  1151. %        ------ NON-BOX ENVIRONMENTS ------
  1152. %
  1153.  
  1154. %
  1155. %    ZED            for non-box multiline formulas
  1156. %
  1157. \def\zed{\z@outnonbox\z@inboxfalse\z@format}
  1158. \def\endzed{\crcr\egroup\endz@env}
  1159. \let\[=\zed
  1160. \def\]{\crcr\egroup$$\ignorespaces}
  1161. %
  1162. %    ARGUE            for algebraic arguments
  1163. %
  1164. %    used for algebraic proofs expressed as extended equations.
  1165. %    like zed but with extra spacing between lines
  1166. %    Generates an alignment display, which may be split across pages.
  1167. %
  1168. \def\argue{\z@outnonbox\interzedlinepenalty=\interdisplaylinepenalty
  1169.     \openup 1\jot \z@format
  1170.     \noalign{\vskip-\jot}}% equal vspace above and below argue display
  1171. \let\endargue=\endzed
  1172. %
  1173. %    INFRULE            for inference rules
  1174. %
  1175. %    used for inference rules. The horizontal line is generated by \derive:
  1176. %    an optional argument contains the side-conditions of the rule.
  1177. %
  1178. \def\infrule{\z@outnonbox\halign\bgroup
  1179.     \zstrut\quad$\@lign##$\quad\hfil&\quad\@lign##\hfil\cr}
  1180. \let\endinfrule=\endzed
  1181. \def\derive{\crcr\also\@but\omit\z@hrulefill%
  1182.     \@ifnextchar[{\z@sidecondition}{\cr\also\@but}}
  1183. \def\Derive{\crcr\also\@but\omit\z@hrulefill\cr\@but
  1184.         \noalign{\kern-\dp\zstrutbox
  1185.     \kern\doublerulesep \nobreak}%
  1186. \omit\derive}
  1187. \def\z@sidecondition[#1]{&$\smash{\lower 0.2ex\hbox{$[\;#1\;]$}}$\cr\also\@but}
  1188. %
  1189. %    SYNTAX            for syntax rules
  1190. %
  1191. % `syntax' environment: used for syntax rules - even (once!) for VDM.
  1192. \def\syntax{\z@outnonbox\halign\bgroup
  1193.     \zstrut$\@lign##$\hfil &\hfil$\@lign{}##{}$\hfil
  1194.     &$\@lign##$\hfil &\qquad\@lign-- ##\hfil\cr}
  1195. \let\endsyntax=\endzed
  1196.  
  1197. %
  1198. %        ------ BOXED ENVIRONMENTS ------
  1199. %
  1200. %
  1201. %    SCHEMA            schema definitions
  1202. %
  1203. \def\schema#1{\z@inoutbox\z@topline{$\,#1\,$}}
  1204. \def\endschema{\z@botline \endzed \z@makeinner \z@nopar}
  1205. %
  1206. %    SCHEMA*            schema with no name
  1207. %
  1208. \@namedef{schema*}{\leftnamesfalse\z@inoutbox\z@topline{}}
  1209. \expandafter\let\csname endschema*\endcsname=\endschema
  1210. %
  1211. %    GENSCHEMA        generic schema definitions
  1212. %
  1213. \def\genschema#1#2{\z@inoutbox\z@topline{$\,#1\:[#2]\,$}}
  1214. \let\endgenschema=\endschema
  1215. %
  1216. %    AXDEF            'liberal' axiomatic definitions
  1217. %
  1218. \def\axdef{\z@inoutbox}
  1219. \def\endaxdef{\endzed\z@makeinner}
  1220. %
  1221. %    UNIQDEF            'unique' axiomatic definitions
  1222. %
  1223. \def\uniqdef{\leftnamesfalse\z@inoutbox\z@dbltopline{}}
  1224. \let\enduniqdef=\endschema
  1225. %
  1226. %    GENDEF            'generic' axiomatic definitions
  1227. %
  1228. % HACK TO  MAKE IT COMPATIBLE WITH FUZZ.STY
  1229. %
  1230. \def\gendef{\@ifnextchar[{\z@gendef}{\z@@gendef}}
  1231. \def\z@gendef[#1]{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,[#1]\,$}}
  1232. \def\z@@gendef#1{\leftnamesfalse\z@inoutbox\z@dbltopline{$\,[#1]\,$}}
  1233. \let\endgendef=\endschema
  1234. %
  1235. %    CLASS
  1236. %
  1237. \def\class#1{\z@leavevmode\z@makeouter\z@inclasstrue
  1238.         \z@boxenv\z@topline{$\,#1\,$}}
  1239. \let\endclass\endschema
  1240. %
  1241. %    OP
  1242. %
  1243. \def\op{\z@inclasscheck\schema}
  1244. \let\endop\endschema
  1245. %
  1246. %    STATE
  1247. %
  1248. \def\state{\z@inclasscheck\vbox\bgroup\vskip-\ht\zstrutbox\vbox\bgroup\hbox\bgroup\@nameuse{schema*}}
  1249. \def\endstate{\endschema\egroup\egroup\egroup}
  1250. %
  1251. %    INIT
  1252. %
  1253. \def\init{\z@inclasscheck\schema{\Init}}
  1254. \let\endinit\endschema
  1255. %
  1256. %    CONST
  1257. %
  1258. \let\const\axdef
  1259. \let\endconst\endaxdef
  1260. %
  1261. %    TYPE
  1262. %
  1263. \def\type{\z@inclasscheck}
  1264. \let\endtype\relax
  1265. %
  1266. %        ------ OTHER ENVIRONMENTS ------
  1267. %
  1268. %    SIDEBYSIDE
  1269. %
  1270. % This should support an arbitary number of columns
  1271. %    \zedindent's proportion of \linewidth gives a practical limit
  1272. %
  1273. \def\sidebyside{\@ifnextchar[{\z@columns}{\z@columns[2]}}
  1274. \def\z@columns[#1]{\z@leavevmode\z@cols#1 \z@makeouter\z@narrow%
  1275.     $$\lineskip=0pt\z@incolstrue
  1276.     \predisplaysize\maxdimen
  1277.     \ifz@leftmargin\hskip-\zedindent\z@leftmarginfalse\fi
  1278.     \setbox0=\hbox to \linewidth\bgroup\z@zeroskips%
  1279.     \divide\zedbar by \z@cols \divide\zedleftsep by \z@cols
  1280.     \divide\zedtab by \z@cols \divide\linewidth by \z@cols
  1281.     \parbox[t]{\linewidth}\bgroup\z@wide}
  1282. %
  1283. \def\nextside{\egroup\hss\parbox[t]{\linewidth}\bgroup\z@wide}
  1284. %
  1285. \newdimen\z@temp
  1286. \def\endsidebyside{\egroup\egroup
  1287.     \z@temp\ht0 \advance\z@temp by \dp0\advance\z@temp by-\dp\zstrutbox
  1288.     \hbox{\raise\z@temp\box0}\endz@env\z@makeinner\z@nopar}
  1289. %
  1290. %    ZPAR
  1291. %
  1292. \def\zpar{\z@leavevmode
  1293.     \ifz@inenv\z@inclasstrue\fi% fudge to let zpar in all boxes
  1294.     \z@makeouter\z@changesize
  1295.     \advance\linewidth by -\z@curindent
  1296.     \advance\linewidth by -\wd\z@curline
  1297.     \hskip-\wd\z@curline\advance\linewidth by -\zedindent$$
  1298.     \ifz@leftmargin\hskip-\zedindent\fi% adjustment for first column
  1299.     \advance\displayindent by \zedindent
  1300.     \advance\displaywidth by -\zedindent
  1301.     \advance\displayindent by \z@curindent
  1302.     \advance\displayindent by \wd\z@curline
  1303.     \advance\displaywidth by -\z@curindent
  1304.     \advance\displaywidth by -\wd\z@curline
  1305.     \global\setbox\z@curline\hbox{}
  1306.     \z@narrow\parbox[b]{\linewidth}\bgroup\hfil\break}
  1307. \def\endzpar{\egroup$$\z@makeinner\z@nopar}
  1308. %
  1309. %    CLASSCOM
  1310. %
  1311. \def \classcom{\zpar\sf}
  1312. \let \endclasscom=\endzpar
  1313. %
  1314. %    PROOF
  1315. %
  1316. \def\proof{\zpar$\PR$\zpar}
  1317. \def\endproof{\endzpar\endzpar}
  1318. %
  1319. % Additional auxiliary macros
  1320. %
  1321. \def\zseq#1{\lseq #1 \rseq}
  1322. \def\zset#1{\{ #1 \}}
  1323. \def\zimg#1{\limg #1 \rimg}
  1324. \def\zsch#1{\lsch #1 \rsch}
  1325. \def\zimgset#1{\zimg{\zset{#1}}}
  1326. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  1327. %
  1328. %    OZ        FUZZ
  1329. %
  1330. %    \defs        ==
  1331. %    \sdef        \defs
  1332. %
  1333. \def\fuzzcompatible{%
  1334. \let\defs\sdef
  1335. \let\empty\emptyset
  1336. }
  1337. %
  1338. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  1339. %%%%%
  1340. %%%%%        FUTURE UPDATES:
  1341. %%%%%
  1342. %%%%% investigate the setting of \par to minimise space after schemas & zpars
  1343. %%%%% make display skips bigger for large fonts
  1344. %%%%%
  1345. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  1346.  
  1347.