changed beginning of "Reading a new theory", added index "automatic loading"
authorclasohm
Thu Nov 25 14:32:54 1993 +0100 (1993-11-25)
changeset 150919a03a587eb
parent 149 caa7a52ff46f
child 151 c5e636ca6576
changed beginning of "Reading a new theory", added index "automatic loading"
doc-src/Ref/ref.toc
doc-src/Ref/theories.tex
     1.1 --- a/doc-src/Ref/ref.toc	Thu Nov 25 14:23:04 1993 +0100
     1.2 +++ b/doc-src/Ref/ref.toc	Thu Nov 25 14:32:54 1993 +0100
     1.3 @@ -105,46 +105,47 @@
     1.4  \contentsline {subsection}{Other meta-rules}{42}
     1.5  \contentsline {chapter}{\numberline {6}Theories, Terms and Types}{44}
     1.6  \contentsline {section}{\numberline {6.1}Defining Theories}{44}
     1.7 +\contentsline {subsection}{Classes and types}{47}
     1.8  \contentsline {section}{\numberline {6.2}Loading Theories}{47}
     1.9  \contentsline {subsection}{Reading a new theory}{47}
    1.10 -\contentsline {subsection}{Filenames and paths}{47}
    1.11 -\contentsline {subsection}{Reloading a theory}{47}
    1.12 +\contentsline {subsection}{Filenames and paths}{48}
    1.13 +\contentsline {subsection}{Reloading a theory}{48}
    1.14  \contentsline {subsection}{Pseudo theories}{48}
    1.15 -\contentsline {subsection}{Removing a theory}{48}
    1.16 -\contentsline {subsection}{Using Poly/{\psc ml}}{48}
    1.17 +\contentsline {subsection}{Removing a theory}{49}
    1.18 +\contentsline {subsection}{Using Poly/{\psc ml}}{49}
    1.19  \contentsline {section}{\numberline {6.3}Basic operations on theories}{49}
    1.20  \contentsline {subsection}{Extracting an axiom from a theory}{49}
    1.21 -\contentsline {subsection}{Building a theory}{49}
    1.22 -\contentsline {subsection}{Inspecting a theory}{50}
    1.23 -\contentsline {section}{\numberline {6.4}Terms}{51}
    1.24 -\contentsline {section}{\numberline {6.5}Certified terms}{52}
    1.25 -\contentsline {subsection}{Printing terms}{52}
    1.26 -\contentsline {subsection}{Making and inspecting certified terms}{52}
    1.27 -\contentsline {section}{\numberline {6.6}Types}{53}
    1.28 -\contentsline {section}{\numberline {6.7}Certified types}{53}
    1.29 -\contentsline {subsection}{Printing types}{53}
    1.30 -\contentsline {subsection}{Making and inspecting certified types}{53}
    1.31 -\contentsline {chapter}{\numberline {7}Substitution Tactics}{55}
    1.32 -\contentsline {section}{\numberline {7.1}Simple substitution}{55}
    1.33 -\contentsline {section}{\numberline {7.2}Substitution in the hypotheses}{56}
    1.34 -\contentsline {section}{\numberline {7.3}Setting up {\ptt hyp_subst_tac}}{56}
    1.35 -\contentsline {chapter}{\numberline {8}Simplification}{59}
    1.36 -\contentsline {section}{\numberline {8.1}Simplification sets}{59}
    1.37 -\contentsline {subsection}{Rewrite rules}{59}
    1.38 -\contentsline {subsection}{Congruence rules}{60}
    1.39 -\contentsline {subsection}{The subgoaler}{60}
    1.40 -\contentsline {subsection}{The solver}{61}
    1.41 -\contentsline {subsection}{The looper}{61}
    1.42 -\contentsline {section}{\numberline {8.2}The simplification tactics}{62}
    1.43 -\contentsline {section}{\numberline {8.3}Example: using the simplifier}{63}
    1.44 -\contentsline {chapter}{\numberline {9}The classical theorem prover}{66}
    1.45 -\contentsline {section}{\numberline {9.1}The sequent calculus}{66}
    1.46 -\contentsline {section}{\numberline {9.2}Simulating sequents by natural deduction}{67}
    1.47 -\contentsline {section}{\numberline {9.3}Extra rules for the sequent calculus}{68}
    1.48 -\contentsline {section}{\numberline {9.4}Classical rule sets}{69}
    1.49 -\contentsline {section}{\numberline {9.5}The classical tactics}{70}
    1.50 -\contentsline {subsection}{Single-step tactics}{71}
    1.51 -\contentsline {subsection}{The automatic tactics}{71}
    1.52 -\contentsline {subsection}{Other useful tactics}{71}
    1.53 -\contentsline {subsection}{Creating swapped rules}{72}
    1.54 -\contentsline {section}{\numberline {9.6}Setting up the classical prover}{72}
    1.55 +\contentsline {subsection}{Building a theory}{50}
    1.56 +\contentsline {subsection}{Inspecting a theory}{51}
    1.57 +\contentsline {section}{\numberline {6.4}Terms}{52}
    1.58 +\contentsline {section}{\numberline {6.5}Certified terms}{53}
    1.59 +\contentsline {subsection}{Printing terms}{53}
    1.60 +\contentsline {subsection}{Making and inspecting certified terms}{53}
    1.61 +\contentsline {section}{\numberline {6.6}Types}{54}
    1.62 +\contentsline {section}{\numberline {6.7}Certified types}{54}
    1.63 +\contentsline {subsection}{Printing types}{54}
    1.64 +\contentsline {subsection}{Making and inspecting certified types}{54}
    1.65 +\contentsline {chapter}{\numberline {7}Substitution Tactics}{56}
    1.66 +\contentsline {section}{\numberline {7.1}Simple substitution}{56}
    1.67 +\contentsline {section}{\numberline {7.2}Substitution in the hypotheses}{57}
    1.68 +\contentsline {section}{\numberline {7.3}Setting up {\ptt hyp_subst_tac}}{57}
    1.69 +\contentsline {chapter}{\numberline {8}Simplification}{60}
    1.70 +\contentsline {section}{\numberline {8.1}Simplification sets}{60}
    1.71 +\contentsline {subsection}{Rewrite rules}{60}
    1.72 +\contentsline {subsection}{Congruence rules}{61}
    1.73 +\contentsline {subsection}{The subgoaler}{61}
    1.74 +\contentsline {subsection}{The solver}{62}
    1.75 +\contentsline {subsection}{The looper}{62}
    1.76 +\contentsline {section}{\numberline {8.2}The simplification tactics}{63}
    1.77 +\contentsline {section}{\numberline {8.3}Example: using the simplifier}{64}
    1.78 +\contentsline {chapter}{\numberline {9}The classical theorem prover}{67}
    1.79 +\contentsline {section}{\numberline {9.1}The sequent calculus}{67}
    1.80 +\contentsline {section}{\numberline {9.2}Simulating sequents by natural deduction}{68}
    1.81 +\contentsline {section}{\numberline {9.3}Extra rules for the sequent calculus}{69}
    1.82 +\contentsline {section}{\numberline {9.4}Classical rule sets}{70}
    1.83 +\contentsline {section}{\numberline {9.5}The classical tactics}{71}
    1.84 +\contentsline {subsection}{Single-step tactics}{72}
    1.85 +\contentsline {subsection}{The automatic tactics}{72}
    1.86 +\contentsline {subsection}{Other useful tactics}{72}
    1.87 +\contentsline {subsection}{Creating swapped rules}{73}
    1.88 +\contentsline {section}{\numberline {9.6}Setting up the classical prover}{73}
     2.1 --- a/doc-src/Ref/theories.tex	Thu Nov 25 14:23:04 1993 +0100
     2.2 +++ b/doc-src/Ref/theories.tex	Thu Nov 25 14:32:54 1993 +0100
     2.3 @@ -173,25 +173,21 @@
     2.4  \label{LoadingTheories}
     2.5  \subsection{Reading a new theory}
     2.6  
     2.7 -\begin{ttbox} 
     2.8 -use_thy: string -> unit
     2.9 -\end{ttbox}
    2.10  Each theory definition must reside in a separate file.  Let the file {\it
    2.11    tf}{\tt.thy} contain the definition of a theory called $TF$ with parent
    2.12  theories $TB@1$ \dots $TB@n$.  Calling \ttindexbold{use_thy}~{\tt"}{\it
    2.13    TF\/}{\tt"} reads file {\it tf}{\tt.thy}, writes an intermediate {\ML}-file
    2.14 -{\tt.}{\it tf}{\tt.thy.ML}, and reads the latter file.  Any of the parent
    2.15 -theories that have not been loaded yet are read now by recursive {\tt
    2.16 -  use_thy} calls until either an already loaded theory or {\tt Pure} is
    2.17 -reached.  Therefore one can read a complete logic by just one {\tt use_thy}
    2.18 -call if all theories are linked appropriatly.  Afterwards an {\ML}
    2.19 +{\tt.}{\it tf}{\tt.thy.ML}, and reads the latter file. \indexbold{automatic
    2.20 +loading}  Any of the parent theories that have not been loaded yet are read now
    2.21 +by recursive {\tt use_thy} calls until either an already loaded theory or {\tt
    2.22 +  Pure} is reached.  Therefore one can read a complete logic by just one {\tt
    2.23 +use_thy} call if all theories are linked appropriatly.  Afterwards an {\ML}
    2.24  structure~$TF$ containing a component {\tt thy} for the new theory and
    2.25  components $r@1$ \dots $r@n$ for the rules is declared; it also contains the
    2.26  definitions of the {\tt ML} section if any. Unless
    2.27 -\ttindexbold{delete_tmpfiles} is set to {\tt false}, {\tt.}{\it
    2.28 -  tf}{\tt.thy.ML} is deleted if no errors occured. Finally the file {\it
    2.29 -  tf}{\tt.ML} is read, if it exists; this file normally contains proofs
    2.30 -involving the new theory.
    2.31 +\ttindexbold{delete_tmpfiles} is set to {\tt false}, {\tt.}{\it tf}{\tt.thy.ML}
    2.32 +is deleted if no errors occured. Finally the file {\it tf}{\tt.ML} is read, if
    2.33 +it exists; this file normally contains proofs involving the new theory.
    2.34  
    2.35  
    2.36  \subsection{Filenames and paths}