# HG changeset patch # User wenzelm # Date 1346152515 -7200 # Node ID 1fead823c7c61bf9515695cd6058df5a8c7a02af # Parent 3ec847562782934b7dc6c51c3f10e8e77caead4b removed old stuff; diff -r 3ec847562782 -r 1fead823c7c6 doc-src/CHANGES-93.txt --- a/doc-src/CHANGES-93.txt Tue Aug 28 13:12:03 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,90 +0,0 @@ -**** Isabelle-93 : a faster version of Isabelle-92 **** - -Isabelle now runs faster through a combination of improvements: pattern -unification, discrimination nets and removal of assumptions during -simplification. A new simplifier, although less flexible than the old one, -runs many times faster for large subgoals. Classical reasoning -(e.g. fast_tac) runs up to 30% faster when large numbers of rules are -involved. Incompatibilities are few, and mostly concern the simplifier. - -THE SPEEDUPS - -The new simplifier is described in the Reference Manual, Chapter 8. See -below for advice on converting. - -Pattern unification is completely invisible to users. It efficiently -handles a common case of higher-order unification. - -Discrimination nets replace the old stringtrees. They provide fast lookup -in a large set of rules for matching or unification. New "net" tactics -replace the "compat_..." tactics based on stringtrees. Tactics -biresolve_from_nets_tac, bimatch_from_nets_tac, resolve_from_net_tac and -match_from_net_tac take a net, rather than a list of rules, and perform -resolution or matching. Tactics net_biresolve_tac, net_bimatch_tac -net_resolve_tac and net_match_tac take a list of rules, build a net -(internally) and perform resolution or matching. - -The tactical METAHYPS, which allows a subgoal's hypotheses to be taken as a -list of theorems, has been extended to handle unknowns (although not type -unknowns). The simplification tactics now use METAHYPS to economise on -storage consumption, and to avoid problems involving "parameters" bound in -a subgoal. The modified simplifier now requires the auto_tac to take an -extra argument: a list of theorems, which represents the assumptions of the -current subgoal. - -OTHER CHANGES - -Apart from minor improvements in Pure Isabelle, the main other changes are -extensions to object-logics. HOL now contains a treatment of co-induction -and co-recursion, while ZF contains a formalization of equivalence classes, -the integers and binary arithmetic. None of this material is documented. - - -CONVERTING FROM THE OLD TO THE NEW SIMPLIFIER (for FOL/ZF/LCF/HOL) - -1. Run a crude shell script to convert your ML-files: - - change_simp *ML - -2. Most congruence rules are no longer needed. Hence you should remove all -calls to mk_congs and mk_typed_congs (they no longer exist) and most -occurrences of addcongs. The only exception are congruence rules for special -constants like (in FOL) - -[| ?P <-> ?P'; ?P' ==> ?Q <-> ?Q' |] ==> ?P --> ?Q = ?P' --> ?Q' -and -[| A=A'; !!x. x:A' ==> P(x) <-> P'(x) |] ==> -(ALL x:A. P(x)) <-> (ALL x:A'. P'(x)) - -where some of the arguments are simplified under additional premises. Most -likely you don't have any constructs like that, or they are already included -in the basic simpset. - -3. In case you have used the addsplits facilities of the old simplifier: -The case-splitting and simplification tactics have been separated. If you -want to interleave case-splitting with simplification, you have do so -explicitly by the following command: - -ss setloop (split_tac split_thms) - -where ss is a simpset and split_thms the list of case-splitting theorems. -The shell script in step 1 tries to convert to from addsplits to setloop -automatically. - -4. If you have used setauto, you have to change it to setsolver by hand. -The solver is more delicate than the auto tactic used to be. For details see -the full description of the new simplifier. One very slight incompatibility -is the fact that the old auto tactic could sometimes see premises as part of -the proof state, whereas now they are always passed explicit as arguments. - -5. It is quite likely that a few proofs require further hand massaging. - -Known incompatibilities: -- Applying a rewrite rule cannot instantiate a subgoal. This rules out -solving a premise of a conditional rewrite rule with extra unknowns by -rewriting. Only the solver can instantiate. - -Known bugs: -- The names of bound variables can be changed by the simplifier. - - diff -r 3ec847562782 -r 1fead823c7c6 doc-src/ERRATA.txt --- a/doc-src/ERRATA.txt Tue Aug 28 13:12:03 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,129 +0,0 @@ -ERRATA in the book "Isabelle: A Generic Theorem Prover" -by Lawrence C. Paulson (contributions by Tobias Nipkow) - -Some of these errors are typographical but most of them are due to continuing -changes to Isabelle. - -Thanks to Sara Kalvala, Tobias Nipkow - - -INTRODUCTION TO ISABELLE - -Advanced Methods - -page 46: the theory sections can appear in any order - -page 48: theories may now contain a separate definition part - -page 52, middle: the declaration "types bool,nat" should be "types bool nat" - -page 57, bottom: should be addsimps in - val add_ss = FOL_ss addrews [add_0, add_Suc] - - -ISABELLE REFERENCE MANUAL - -Introduction - -page 67: show_brackets is another flag, controlling display of bracketting -show_sorts:=true forces display of types - -Tactics - -page 85: subgoals_tac is another tactic, for multiple calls to subgoal_tac - -Theories - -page 117: the three lines of ML shown can be abbreviated to just - init_thy_reader(); - -page 118: extend_theory has been replaced by numerous functions for adding -types, constants, axioms, etc. - -Defining Logics - - - -page 127: type constraints ("::") now have a very low priority of 4. -As in ML, they must usually be enclosed in paretheses. - -Syntax Transformations - -page 145, line -5: delete repeated "the" in "before the the .thy file" - -Simplification - -page 157 display: Union operator is too big - -page 158, "!": Isabelle now permits more general left-hand sides, so called -higher-order patterns. - -Classical reasoner - -page 176: Classical sets may specify a "wrapper tactical", which can be used -to define addss. The package also provides tactics slow_tac, slow_best_tac, -depth_tac and deepen_tac. - -ISABELLE'S OBJECT-LOGICS - -First-Order Logic - -pages 191, 196: FOL_dup_cs is now deleted (use deepen_tac FOL_cs instead) - -Zermelo-Fraenkel Set Theory - -page 204: type i has class term, not (just) logic - -page 209: axioms have been renamed: - union_iff is now Union_iff - power_set is now Pow_iff - -page 215, bottom of figure 17.10: DiffD2 is now "c : A - B ==> c ~: B" - -page 215, bottom: rules mem_anti_sym and mem_anti_refl are now mem_asym and -mem_irrefl - -page 222, top: missing braces in qconverse_def (around right-hand side) -and QSigma_def (around ) - -page 223, top: lfp_def, gfp_def have missing braces around the argument of -Inter, Union - -page 228: now there is also a theory of cardinal numbers and some -developments involving the Axiom of Choice. - -page 229: now there is another examples directory, IMP (a semantics -equivalence proof for an imperative language) - -Higher-Order Logic - -page 243: Pow is a new constant of type 'a set => 'a set set - -page 246: Pow is defined by Pow(A) == {B. B <= A} -empty_def should be {} == {x.False} - -page 248: Pow has the rules - PowI A<=B ==> A: Pow(B) - PowD A: Pow(B) ==> A<=B - -page 251: split now has type [['a,'b] => 'c, 'a * 'b] => 'c -Definition modified accordingly - -page 252: sum_case now has type ['a=>'c,'b=>'c, 'a+'b] =>'c -Definition and rules modified accordingly - -page 252: HOL_dup_cs is now deleted (use deepen_tac HOL_cs instead) - -page 254: nat_case now has type ['a, nat=>'a, nat] =>'a -Definition modified accordingly - -page 256,258: list_case now takes the list as its last argument, not the -first. - -page 259: HOL theory files may now include datatype declarations, primitive -recursive function definitions, and (co)inductive definitions. These new -sections are available separately at - http://www.cl.cam.ac.uk/users/lcp/archive/ml/HOL-extensions.dvi.gz - -page 259: now there is another examples directory, IMP (a semantics -equivalence proof for an imperative language) diff -r 3ec847562782 -r 1fead823c7c6 doc-src/springer.bbl --- 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} diff -r 3ec847562782 -r 1fead823c7c6 doc-src/springer.tex --- a/doc-src/springer.tex Tue Aug 28 13:12:03 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,110 +0,0 @@ -%% $ lcp Exp $ -\documentstyle[12pt,rail,proof,iman,epsf,mathsing]{book} -%\includeonly{Ref/simplifier} -%% index{\(\w+\)\!meta-level index{meta-\1 -%%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\) [\\ttindexbold{\1} -%% run sedindex springer to prepare index file - -\sloppy - -\title{Isabelle\\A Generic Theorem Prover} -\author{Lawrence C. Paulson\\[2ex] With Contributions by Tobias Nipkow} - -\date{} -\makeindex - -\def\S{Sect.\thinspace}%This is how Springer like it - -\underscoreoff - -\setcounter{secnumdepth}{2} \setcounter{tocdepth}{1} - -\binperiod %%%treat . like a binary operator - -\begin{document} -\maketitle - -\pagenumbering{Roman} -\include{preface} - -\tableofcontents -\newpage -\listoffigures -\newpage - -\markboth{}{} -\newfont{\sanssi}{cmssi12} -\vspace*{2.5cm} -\begin{quote}\raggedleft -{\em To Nathan and Sarah} - -\vspace*{1.2cm} -{\sanssi -You can only find truth with logic\\ -if you have already found truth without it.}\\ -\bigskip - -G.K. Chesterton, {\em The Man who was Orthodox} -\end{quote} - -\thispagestyle{empty} -\newpage -\pagenumbering{arabic} -\part{Introduction to Isabelle} - -\index{hypotheses|see{assumptions}} -\index{rewriting|see{simplification}} -\index{variables!schematic|see{unknowns}} -\index{abstract syntax trees|see{ASTs}} - -\begingroup%things local to Intro -- especially, redefining \part!! -\newcommand\qeq{\stackrel{?}{\equiv}} %for disagreement pairs in unification -\newcommand{\nand}{\mathbin{\lnot\&}} -\newcommand{\xor}{\mathbin{\#}} -\let\part=\chapter -\include{Intro/foundations} -\include{Intro/getting} -\include{Intro/advanced} -\endgroup - -\part{The Isabelle Reference Manual} -\include{Ref/introduction} -\include{Ref/goals} -\include{Ref/tactic} -\include{Ref/tctical} -\include{Ref/thm} -\include{Ref/theories} -\include{Ref/defining} -\include{Ref/syntax} -\include{Ref/substitution} -\include{Ref/simplifier} -\include{Ref/classical} - -\part{Isabelle's Object-Logics} -\newcommand\subcaption[1]{\par {\centering\normalsize\sc#1\par}\bigskip - \hrule\bigskip} -\newenvironment{constants}{\begin{center}\small\begin{tabular}{rrrr}}{\end{tabular}\end{center}} - -\include{Logics/intro} -\include{Logics/FOL} -\include{Logics/ZF} -\include{Logics/HOL} -\include{Logics/LK} -\include{Logics/CTT} - -\include{Ref/theory-syntax} - -%%seealso's must be last so that they appear last in the index entries -\index{backtracking|seealso{{\tt back} command, search}} -\index{classes|seealso{sorts}} -\index{sorts|seealso{arities}} -\index{axioms|seealso{rules, theorems}} -\index{theorems|seealso{rules}} -\index{definitions|seealso{meta-rewriting}} -\index{equality|seealso{simplification}} - -\bibliographystyle{springer} \small\raggedright\frenchspacing -\bibliography{string-abbrv,atp,funprog,general,isabelle,logicprog,theory} - -\printindex -\end{document} diff -r 3ec847562782 -r 1fead823c7c6 doc-src/url.sty --- 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{}", 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:}#1\special{html:}} -% -% 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{|}~