--- a/doc-src/springer.bbl Tue Aug 28 13:12:03 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,334 +0,0 @@
-\begin{thebibliography}{10}
-
-\bibitem{andrews86}
-Andrews, P.~B.,
-\newblock {\em An Introduction to Mathematical Logic and Type Theory: To Truth
- Through Proof},
-\newblock Academic Press, 1986
-
-\bibitem{basin91}
-Basin, D., Kaufmann, M.,
-\newblock The {Boyer-Moore} prover and {Nuprl}: An experimental comparison,
-\newblock In {\em Logical Frameworks}, G.~Huet, G.~Plotkin, Eds. Cambridge
- Univ. Press, 1991, pp.~89--119
-
-\bibitem{boyer86}
-Boyer, R., Lusk, E., McCune, W., Overbeek, R., Stickel, M., Wos, L.,
-\newblock Set theory in first-order logic: Clauses for {G\"odel's} axioms,
-\newblock {\em J. Auto. Reas. {\bf 2}}, 3 (1986), 287--327
-
-\bibitem{bm88book}
-Boyer, R.~S., Moore, J.~S.,
-\newblock {\em A Computational Logic Handbook},
-\newblock Academic Press, 1988
-
-\bibitem{camilleri92}
-Camilleri, J., Melham, T.~F.,
-\newblock Reasoning with inductively defined relations in the {HOL} theorem
- prover,
-\newblock Tech. Rep. 265, Comp. Lab., Univ. Cambridge, Aug. 1992
-
-\bibitem{charniak80}
-Charniak, E., Riesbeck, C.~K., McDermott, D.~V.,
-\newblock {\em Artificial Intelligence Programming},
-\newblock Lawrence Erlbaum Associates, 1980
-
-\bibitem{church40}
-Church, A.,
-\newblock A formulation of the simple theory of types,
-\newblock {\em J. Symb. Logic {\bf 5}\/} (1940), 56--68
-
-\bibitem{coen92}
-Coen, M.~D.,
-\newblock {\em Interactive Program Derivation},
-\newblock PhD thesis, University of Cambridge, 1992,
-\newblock Computer Laboratory Technical Report 272
-
-\bibitem{constable86}
-{Constable et al.}, R.~L.,
-\newblock {\em Implementing Mathematics with the Nuprl Proof Development
- System},
-\newblock Prentice-Hall, 1986
-
-\bibitem{davey&priestley}
-Davey, B.~A., Priestley, H.~A.,
-\newblock {\em Introduction to Lattices and Order},
-\newblock Cambridge Univ. Press, 1990
-
-\bibitem{dawson90}
-Dawson, W.~M.,
-\newblock {\em A Generic Logic Environment},
-\newblock PhD thesis, Imperial College, London, 1990
-
-\bibitem{debruijn72}
-de~Bruijn, N.~G.,
-\newblock Lambda calculus notation with nameless dummies, a tool for automatic
- formula manipulation, with application to the {Church-Rosser Theorem},
-\newblock {\em Indag. Math. {\bf 34}\/} (1972), 381--392
-
-\bibitem{devlin79}
-Devlin, K.~J.,
-\newblock {\em Fundamentals of Contemporary Set Theory},
-\newblock Springer, 1979
-
-\bibitem{coq}
-{Dowek et al.}, G.,
-\newblock The {Coq} proof assistant user's guide,
-\newblock Technical Report 134, INRIA-Rocquencourt, 1991
-
-\bibitem{dummett}
-Dummett, M.,
-\newblock {\em Elements of Intuitionism},
-\newblock Oxford University Press, 1977
-
-\bibitem{dyckhoff}
-Dyckhoff, R.,
-\newblock Contraction-free sequent calculi for intuitionistic logic,
-\newblock {\em J. Symb. Logic {\bf 57}}, 3 (1992), 795--807
-
-\bibitem{felty91a}
-Felty, A.,
-\newblock A logic program for transforming sequent proofs to natural deduction
- proofs,
-\newblock In {\em Extensions of Logic Programming\/} (1991),
- P.~Schroeder-Heister, Ed., Springer, pp.~157--178,
-\newblock LNAI 475
-
-\bibitem{felty93}
-Felty, A.,
-\newblock Implementing tactics and tacticals in a higher-order logic
- programming language,
-\newblock {\em J. Auto. Reas. {\bf 11}}, 1 (1993), 43--82
-
-\bibitem{frost93}
-Frost, J.,
-\newblock A case study of co-induction in {Isabelle HOL},
-\newblock Tech. Rep. 308, Comp. Lab., Univ. Cambridge, Aug. 1993
-
-\bibitem{OBJ}
-Futatsugi, K., Goguen, J., Jouannaud, J.-P., Meseguer, J.,
-\newblock Principles of {OBJ2},
-\newblock In {\em Princ. Prog. Lang.\/} (1985), pp.~52--66
-
-\bibitem{gallier86}
-Gallier, J.~H.,
-\newblock {\em Logic for Computer Science: Foundations of Automatic Theorem
- Proving},
-\newblock Harper \& Row, 1986
-
-\bibitem{mgordon-hol}
-Gordon, M. J.~C., Melham, T.~F.,
-\newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher
- Order Logic},
-\newblock Cambridge Univ. Press, 1993
-
-\bibitem{halmos60}
-Halmos, P.~R.,
-\newblock {\em Naive Set Theory},
-\newblock Van Nostrand, 1960
-
-\bibitem{harper-jacm}
-Harper, R., Honsell, F., Plotkin, G.,
-\newblock A framework for defining logics,
-\newblock {\em J.~ACM {\bf 40}}, 1 (1993), 143--184
-
-\bibitem{haskell-tutorial}
-Hudak, P., Fasel, J.~H.,
-\newblock A gentle introduction to {Haskell},
-\newblock {\em {SIGPLAN} {\bf 27}}, 5 (May 1992)
-
-\bibitem{haskell-report}
-Hudak, P., Jones, S.~P., Wadler, P.,
-\newblock Report on the programming language {Haskell}: A non-strict, purely
- functional language,
-\newblock {\em {SIGPLAN} {\bf 27}}, 5 (May 1992),
-\newblock Version 1.2
-
-\bibitem{huet75}
-Huet, G.~P.,
-\newblock A unification algorithm for typed $\lambda$-calculus,
-\newblock {\em Theoretical Comput. Sci. {\bf 1}\/} (1975), 27--57
-
-\bibitem{huet78}
-Huet, G.~P., Lang, B.,
-\newblock Proving and applying program transformations expressed with
- second-order patterns,
-\newblock {\em Acta Inf. {\bf 11}\/} (1978), 31--55
-
-\bibitem{mural}
-Jones, C.~B., Jones, K.~D., Lindsay, P.~A., Moore, R.,
-\newblock {\em Mural: A Formal Development Support System},
-\newblock Springer, 1991
-
-\bibitem{alf}
-Magnusson, L., {Nordstr\"om}, B.,
-\newblock The {ALF} proof editor and its proof engine,
-\newblock In {\em Types for Proofs and Programs: International Workshop {TYPES
- '93}\/} (published 1994), Springer, pp.~213--237,
-\newblock LNCS 806
-
-\bibitem{mw81}
-Manna, Z., Waldinger, R.,
-\newblock Deductive synthesis of the unification algorithm,
-\newblock {\em Sci. Comput. Programming {\bf 1}}, 1 (1981), 5--48
-
-\bibitem{martin-nipkow}
-Martin, U., Nipkow, T.,
-\newblock Ordered rewriting and confluence,
-\newblock In {\em 10th Conf. Auto. Deduct.\/} (1990), M.~E. Stickel, Ed.,
- Springer, pp.~366--380,
-\newblock LNCS 449
-
-\bibitem{martinlof84}
-Martin-L\"of, P.,
-\newblock {\em Intuitionistic type theory},
-\newblock Bibliopolis, 1984
-
-\bibitem{melham89}
-Melham, T.~F.,
-\newblock Automating recursive type definitions in higher order logic,
-\newblock In {\em Current Trends in Hardware Verification and Automated Theorem
- Proving}, G.~Birtwistle, P.~A. Subrahmanyam, Eds. Springer, 1989,
- pp.~341--386
-
-\bibitem{miller-mixed}
-Miller, D.,
-\newblock Unification under a mixed prefix,
-\newblock {\em J. Symb. Comput. {\bf 14}}, 4 (1992), 321--358
-
-\bibitem{milner-coind}
-Milner, R., Tofte, M.,
-\newblock Co-induction in relational semantics,
-\newblock {\em Theoretical Comput. Sci. {\bf 87}\/} (1991), 209--220
-
-\bibitem{nipkow-prehofer}
-Nipkow, T., Prehofer, C.,
-\newblock Type checking type classes,
-\newblock In {\em 20th Princ. Prog. Lang.\/} (1993), ACM Press, pp.~409--418,
-\newblock Revised version to appear in \bgroup\em J. Func. Prog.\egroup
-
-\bibitem{noel}
-{No\"el}, P.,
-\newblock Experimenting with {Isabelle} in {ZF} set theory,
-\newblock {\em J. Auto. Reas. {\bf 10}}, 1 (1993), 15--58
-
-\bibitem{nordstrom90}
-{Nordstr\"om}, B., Petersson, K., Smith, J.,
-\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction},
-\newblock Oxford University Press, 1990
-
-\bibitem{paulin92}
-Paulin-Mohring, C.,
-\newblock Inductive definitions in the system {Coq}: Rules and properties,
-\newblock Research Report 92-49, LIP, Ecole Normale Sup\'erieure de Lyon, Dec.
- 1992
-
-\bibitem{paulson85}
-Paulson, L.~C.,
-\newblock Verifying the unification algorithm in {LCF},
-\newblock {\em Sci. Comput. Programming {\bf 5}\/} (1985), 143--170
-
-\bibitem{paulson87}
-Paulson, L.~C.,
-\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF},
-\newblock Cambridge Univ. Press, 1987
-
-\bibitem{paulson89}
-Paulson, L.~C.,
-\newblock The foundation of a generic theorem prover,
-\newblock {\em J. Auto. Reas. {\bf 5}}, 3 (1989), 363--397
-
-\bibitem{paulson-COLOG}
-Paulson, L.~C.,
-\newblock A formulation of the simple theory of types (for {Isabelle}),
-\newblock In {\em COLOG-88: International Conference on Computer Logic\/}
- (Tallinn, 1990), P.~Martin-L\"of, G.~Mints, Eds., Estonian Academy of
- Sciences, Springer,
-\newblock LNCS 417
-
-\bibitem{paulson700}
-Paulson, L.~C.,
-\newblock {Isabelle}: The next 700 theorem provers,
-\newblock In {\em Logic and Computer Science}, P.~Odifreddi, Ed. Academic
- Press, 1990, pp.~361--386
-
-\bibitem{paulson91}
-Paulson, L.~C.,
-\newblock {\em {ML} for the Working Programmer},
-\newblock Cambridge Univ. Press, 1991
-
-\bibitem{paulson-coind}
-Paulson, L.~C.,
-\newblock Co-induction and co-recursion in higher-order logic,
-\newblock Tech. Rep. 304, Comp. Lab., Univ. Cambridge, July 1993
-
-\bibitem{paulson-fixedpt}
-Paulson, L.~C.,
-\newblock A fixedpoint approach to implementing (co)inductive definitions,
-\newblock Tech. Rep. 320, Comp. Lab., Univ. Cambridge, Dec. 1993
-
-\bibitem{paulson-set-I}
-Paulson, L.~C.,
-\newblock Set theory for verification: {I}. {From} foundations to functions,
-\newblock {\em J. Auto. Reas. {\bf 11}}, 3 (1993), 353--389
-
-\bibitem{paulson-set-II}
-Paulson, L.~C.,
-\newblock Set theory for verification: {II}. {Induction} and recursion,
-\newblock Tech. Rep. 312, Comp. Lab., Univ. Cambridge, 1993
-
-\bibitem{paulson-final}
-Paulson, L.~C.,
-\newblock A concrete final coalgebra theorem for {ZF} set theory,
-\newblock Tech. rep., Comp. Lab., Univ. Cambridge, 1994
-
-\bibitem{pelletier86}
-Pelletier, F.~J.,
-\newblock Seventy-five problems for testing automatic theorem provers,
-\newblock {\em J. Auto. Reas. {\bf 2}\/} (1986), 191--216,
-\newblock Errata, JAR 4 (1988), 235--236
-
-\bibitem{plaisted90}
-Plaisted, D.~A.,
-\newblock A sequent-style model elimination strategy and a positive refinement,
-\newblock {\em J. Auto. Reas. {\bf 6}}, 4 (1990), 389--402
-
-\bibitem{quaife92}
-Quaife, A.,
-\newblock Automated deduction in {von Neumann-Bernays-G\"odel} set theory,
-\newblock {\em J. Auto. Reas. {\bf 8}}, 1 (1992), 91--147
-
-\bibitem{sawamura92}
-Sawamura, H., Minami, T., Ohashi, K.,
-\newblock Proof methods based on sheet of thought in {EUODHILOS},
-\newblock Research Report IIAS-RR-92-6E, International Institute for Advanced
- Study of Social Information Science, Fujitsu Laboratories, 1992
-
-\bibitem{suppes72}
-Suppes, P.,
-\newblock {\em Axiomatic Set Theory},
-\newblock Dover, 1972
-
-\bibitem{takeuti87}
-Takeuti, G.,
-\newblock {\em Proof Theory}, 2nd~ed.,
-\newblock North Holland, 1987
-
-\bibitem{thompson91}
-Thompson, S.,
-\newblock {\em Type Theory and Functional Programming},
-\newblock Addison-Wesley, 1991
-
-\bibitem{principia}
-Whitehead, A.~N., Russell, B.,
-\newblock {\em Principia Mathematica},
-\newblock Cambridge Univ. Press, 1962,
-\newblock Paperback edition to *56, abridged from the 2nd edition (1927)
-
-\bibitem{wos-bledsoe}
-Wos, L.,
-\newblock Automated reasoning and {Bledsoe's} dream for the field,
-\newblock In {\em Automated Reasoning: Essays in Honor of {Woody Bledsoe}},
- R.~S. Boyer, Ed. Kluwer Academic Publishers, 1991, pp.~297--342
-
-\end{thebibliography}
--- a/doc-src/url.sty Tue Aug 28 13:12:03 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,268 +0,0 @@
-% url.sty ver 1.1 6-Feb-1996 Donald Arseneau asnd@triumf.ca
-%
-% A form of \verb that allows linebreaks at certain characters or
-% combinations of characters, accepts reconfiguration, and can usually
-% be used in the argument to another command. It is intended for email
-% addresses, hypertext links, directories/paths, etc., which normally
-% have no spaces. The font may be selected using the \urlstyle command,
-% and new url-like commands can be defined using \urldef.
-%
-% Usage: Conditions:
-% \url{ } If the argument contains any "%", "#", or "^^", or ends with
-% "\", it can't be used in the argument to another command.
-% The argument must not contain unbalanced braces.
-% \url| | ...where "|" is any character not used in the argument and not
-% "{". The same restrictions as above except that the argument
-% may contain unbalanced braces.
-% \xyz for "\xyz" a defined-url; this can be used anywhere, no matter
-% what characters it contains.
-%
-% See further instructions after "\endinput"
-
-\def\url@ttstyle{%
-\@ifundefined{selectfont}{\def\UrlFont{\tt}}{\def\UrlFont{\ttfamily}}%
-\def\UrlBreaks{\do\.\do\@\do\\\do\/\do\!\do\_\do\|\do\%\do\;\do\>\do\]%
- \do\)\do\,\do\?\do\'\do\+\do\=\do@url@hyp}%
-\def\UrlBigBreaks{\do\:}%
-\def\UrlNoBreaks{\do\(\do\[\do\{\do\<}% (unnecessary)
-\def\UrlSpecials{\do\ {\ }}%
-\def\UrlOrds{\do\*\do\-}% any ordinary characters that aren't usually
-}
-\def\url@rmstyle{%
-\@ifundefined{selectfont}{\def\UrlFont{\rm}}{\def\UrlFont{\rmfamily}}%
-\def\UrlBreaks{\do\.\do\@\do\/\do\!\do\%\do\;\do\]\do\)\do\,\do\?\do@url@hyp
- \do\+\do\=}%
-\def\UrlBigBreaks{\do\:}%
-\def\UrlNoBreaks{\do\(\do\[\do\{}% prevents breaks after *next* character
-\def\UrlSpecials{\do\<{\langle}\do\>{\rangle\penalty\relpenalty}\do\_{\_%
- \penalty\@m}\do\|{\mid}\do\{{\lbrace}\do\}{\rbrace\penalty\relpenalty}\do
- \\{\mathbin{\backslash}}\do\~{\mathord{{}^{\textstyle\sim}}}\do\ {\ }}%
-\def\UrlOrds{\do\'\do\"\do\-}%
-}
-\def\url@sfstyle{\url@rmstyle
-\@ifundefined{selectfont}{\def\UrlFont{\sf}}{\def\UrlFont{\sffamily}}%
-}
-\def\url@samestyle{\ifdim\fontdimen\thr@@\font=\z@ \url@ttstyle \else
- \url@rmstyle \fi \def\UrlFont{}}
-
-\def\do@url@hyp{}% by default, no breaks after hyphens
-
-\@ifundefined{strip@prefix}{\def\strip@prefix#1>{}}{}
-\@ifundefined{verbatim@nolig@list}{\def\verbatim@nolig@list{\do\`}}{}
-
-\def\Url{\relax\ifmmode\@nomatherr$\fi
- \UrlFont $\fam\z@ \textfont\z@\font
- \let\do\@makeother \dospecials % verbatim catcodes
- \catcode`{\@ne \catcode`}\tw@ % except braces
- \medmuskip0mu \thickmuskip\medmuskip \thinmuskip\medmuskip
- \@tempcnta\fam\multiply\@tempcnta\@cclvi
- \let\do\set@mathcode \UrlOrds % ordinary characters that were special
- \advance\@tempcnta 8192 \UrlBreaks % bin
- \advance\@tempcnta 4096 \UrlBigBreaks % rel
- \advance\@tempcnta 4096 \UrlNoBreaks % open
- \let\do\set@mathact \UrlSpecials % active
- \let\do\set@mathnolig \verbatim@nolig@list % prevent ligatures
- \@ifnextchar\bgroup\Url@z\Url@y}
-
-\def\Url@y#1{\catcode`{11 \catcode`}11
- \def\@tempa##1#1{\Url@z{##1}}\@tempa}
-\def\Url@z#1{\def\@tempa{#1}\expandafter\expandafter\expandafter\Url@use
- \expandafter\strip@prefix\meaning\@tempa\, \relax\m@th$\endgroup}
-\let\Url@use\@empty
-
-\def\set@mathcode#1{\count@`#1\advance\count@\@tempcnta\mathcode`#1\count@}
-\def\set@mathact#1#2{\mathcode`#132768 \lccode`\~`#1\lowercase{\def~{#2}}}
-\def\set@mathnolig#1{\ifnum\mathcode`#1<32768
- \lccode`\~`#1\lowercase{\edef~{\mathchar\number\mathcode`#1_{\/}}}%
- \mathcode`#132768 \fi}
-
-\def\urldef#1#2{\begingroup \setbox\z@\hbox\bgroup
- \def\Url@z{\Url@def{#1}{#2}}#2}
-\expandafter\ifx\csname DeclareRobustCommand\endcsname\relax
- \def\Url@def#1#2#3{\m@th$\endgroup\egroup\endgroup
- \def#1{#2{#3}}}
-\else
- \def\Url@def#1#2#3{\m@th$\endgroup\egroup\endgroup
- \DeclareRobustCommand{#1}{#2{#3}}}
-\fi
-
-\def\urlstyle#1{\csname url@#1style\endcsname}
-
-% Sample (and default) configuration:
-%
-\newcommand\url{\begingroup \Url}
-%
-\newcommand\path{\begingroup \urlstyle{tt}\Url}
-%
-% too many styles define \email like \address, so I will not define it.
-% \newcommand\email{\begingroup \urlstyle{rm}\Url}
-
-% Process LaTeX \package options
-%
-\urlstyle{tt}
-\@ifundefined{ProvidesPackage}{}{
- \ProvidesPackage{url}[1996/02/06 \space ver 1.1 \space
- Verb mode for urls, email addresses, and file names]
- \DeclareOption{hyphens}{\def\do@url@hyp{\do\-}}% allow breaks after hyphens
- \DeclareOption{obeyspaces}{\let\Url@use\relax}
- \ProcessOptions
-\ifx\Url@use\relax \def\Url@use#1 #2{#1\ifx\relax#2\@empty\else
- \penalty\relpenalty\ #2\expandafter\Url@use\fi}\fi
-}
-
-\endinput
-%
-% url.sty ver 1.1 6-Feb-1996 Donald Arseneau asnd@reg.triumf.ca
-%
-% This package defines "\url", a form of "\verb" that allows linebreaks,
-% and can often be used in the argument to another command. It can be
-% configured to print in different formats, and is particularly useful for
-% hypertext links, email addresses, directories/paths, etc. The font may
-% be selected using the "\urlstyle" command and pre-defined text can be
-% stored with the "\urldef" command. New url-like commands can be defined,
-% and a "\path" command is provided this way.
-%
-% Usage: Conditions:
-% \url{ } If the argument contains any "%", "#", or "^^", or ends with
-% "\", it can't be used in the argument to another command.
-% The argument must not contain unbalanced braces.
-% \url| | ...where "|" is any character not used in the argument and not
-% "{". The same restrictions as above except that the argument
-% may contain unbalanced braces.
-% \xyz for "\xyz" a defined-url; this can be used anywhere, no matter
-% what characters it contains.
-%
-% The "\url" command is fragile, and its argument is likely to be very
-% fragile, but a defined-url is robust.
-%
-% Package Option: obeyspaces
-% Ordinarily, all spaces are ignored in the url-text. The "[obeyspaces]"
-% option allows spaces, but may introduce spurious spaces when a url
-% containing "\" characters is given in the argument to another command.
-% So if you need to obey spaces should say "\usepackage[obeyspaces]{url}",
-% and if you need both spaces and backslashes, use a `defined-url' for
-% anything with "\".
-%
-% Package Option: hyphens
-% Ordinarily, breaks are not allowed after "-" characters because this
-% leads to confusion. (Is the "-" part of the address or just a hyphen?)
-% The package option "[hyphens]" allows breaks after explicit hyphen
-% characters. The "\url" command will *never ever* hyphenate words.
-%
-% Defining a defined-url:
-% Take for example the email address "myself%node@gateway.net" which could
-% not be given (using "\url" or "\verb") in a caption or parbox due to the
-% percent sign. This address can be predefined with
-% \urldef{\myself}\url{myself%node@gateway.net} or
-% \urldef{\myself}\url|myself%node@gateway.net|
-% and then you may use "\myself" instead of "\url{myself%node@gateway.net}"
-% in an argument, and even in a moving argument like a caption because a
-% defined-url is robust.
-%
-% Style:
-% You can switch the style of printing using "\urlstyle{tt}", where "tt"
-% can be any defined style. The pre-defined styles are "tt", "rm", "sf",
-% and "same" which all allow the same linebreaks but different fonts --
-% the first three select a specific font and the "same" style uses the
-% current text font. You can define your own styles with different fonts
-% and/or line-breaking by following the explanations below. The "\url"
-% command follows whatever the currently-set style dictates.
-%
-% Alternate commands:
-% It may be desireable to have different things treated differently, each
-% in a predefined style; e.g., if you want directory paths to always be
-% in tt and email addresses to be rm, then you would define new url-like
-% commands as follows:
-%
-% \newcommand\email{\begingroup \urlstyle{rm}\Url}
-% \newcommand\directory{\begingroup \urlstyle{tt}\Url}
-%
-% You must follow this format closely, and NOTE that the final command is
-% "\Url", not "\url". In fact, the "\directory" example is exactly the
-% "\path" definition which is pre-defined in the package. If you look
-% above, you will see that "\url" is defined with
-% \newcommand\url{\begingroup \Url}
-% I.e., using whatever url-style has been selected.
-%
-% You can make a defined-url for these other styles, using the usual
-% "\urldef" command as in this example:
-%
-% \urldef{\myself}{\email}{myself%node.domain@gateway.net}
-%
-% which makes "\myself" act like "\email{myself%node.domain@gateway.net}",
-% if the "\email" command is defined as above. The "\myself" command is
-% robust.
-%
-% Defining styles:
-% Before describing how to customize the printing style, it is best to
-% mention something about the unusual implementation of "\url". Although
-% the material is textual in nature, and the font specification required
-% is a text-font command, the text is actually typeset in *math* mode.
-% This allows the context-sensitive linebreaking, but also accounts for
-% the default behavior of ignoring spaces. Now on to defining styles.
-%
-% To change the font or the list of characters that allow linebreaks, you
-% could redefine the commands "\UrlFont", "\UrlBreaks", "\UrlSpecials" etc.
-% directly in the document, but it is better to define a new `url-style'
-% (following the example of "\url@ttstyle" and "\url@rmstyle") which defines
-% all of "\UrlBigbreaks", "\UrlNoBreaks", "\UrlBreaks", "\UrlSpecials", and
-% "\UrlFont".
-%
-% Changing font:
-% The "\UrlFont" command selects the font. The definition of "\UrlFont"
-% done by the pre-defined styles varies to cope with a variety of LaTeX
-% font selection schemes, but it could be as simple as "\def\UrlFont{\tt}".
-% In addition to setting "\UrlFont", some characters will probably need
-% to be defined in the "\UrlSpecials" list because most fonts don't have
-% all the standard input characters. See the definition of "\url@rmstyle",
-% which implements "\urlstyle{rm}". Or even better, follow the definition
-% of "\url@sfstyle", which executes "\url@rmstyle" and then redefines
-% just "\UrlFont". The nominal format for each special character "c"
-% in the "\UrlSpecials" list is: "\do\c{<definition>}", but you can
-% include other definitions too.
-%
-% Changing linebreaks:
-% The list of characters that allow line-breaks is given by "\UrlBreaks"
-% and "\UrlBigBreaks", which have the format "\do\c" for character "c".
-% The differences are that `BigBreaks' have a lower penalty and have
-% different breakpoints when in sequence (as in "http://"): `BigBreaks'
-% are treated as mathrels while `Breaks' are mathbins (see The TeXbook,
-% p.170). In particular, a series of `BigBreak' characters will break at
-% the end and only at the end; a series of `Break' characters will break
-% after the first and after every following *pair*; there will be no
-% break after a `Break' character if a `BigBreak' follows. In the case
-% of "http://" it doesn't matter whether ":" is a `Break' or `BigBreak' --
-% the breaks are the same in either case; but for DECnet nodes with "::"
-% it is important to prevent breaks *between* the colons, and that is why
-% colons are `BigBreaks'.
-%
-% It is possible for characters to prevent breaks after the next following
-% character (I use this for parentheses). Specify these in "\UrlNoBreaks".
-%
-% You can do arbitrarily complex things with characters by making them
-% active in math mode (mathcode hex-8000) and specifying the definition(s)
-% in "\UrlSpecials". This is used in the rm and sf styles to handle
-% several characters that are not present in fonts.
-%
-% If all this sounds confusing ... well, it is! But I hope you won't need
-% to redefine breakpoints -- the default assignments seem to work well for
-% a wide variety of applications. If you do need to make changes, you can
-% test for breakpoints using regular math mode and the characters "+=(a".
-%
-% Yet more flexibility:
-% You can also set up url.sty to do multiple things with the verbatim text
-% by defining "\Url@use", but the format of the definition is special:
-%
-% \def\Url@use#1\,{ ... do things with #1 ... }
-%
-% Yes, that is "#1" followed by "\," then the definition. For example,
-% to put a hypertext link in the DVI file:
-%
-% \def\Url@use#1\,{\special{html:<a href="#1">}#1\special{html:</a>}}
-%
-% The End
-% ver 1.1 6-Feb-1996:
-% Fix hyphens that wouldn't break and ligatures that weren't suppressed.
-
-Test file integrity: ASCII 32-57, 58-126: !"#$%&'()*+,-./0123456789
-:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~