doc-src/Ref/ref.toc
 changeset 152 37025f8608a6 parent 150 919a03a587eb child 359 b5a2e9503a7a
equal inserted replaced
151:c5e636ca6576 152:37025f8608a6
`   134 \contentsline {subsection}{Rewrite rules}{60}`
`   134 \contentsline {subsection}{Rewrite rules}{60}`
`   135 \contentsline {subsection}{Congruence rules}{61}`
`   135 \contentsline {subsection}{Congruence rules}{61}`
`   136 \contentsline {subsection}{The subgoaler}{61}`
`   136 \contentsline {subsection}{The subgoaler}{61}`
`   137 \contentsline {subsection}{The solver}{62}`
`   137 \contentsline {subsection}{The solver}{62}`
`   138 \contentsline {subsection}{The looper}{62}`
`   138 \contentsline {subsection}{The looper}{62}`
`   139 \contentsline {section}{\numberline {8.2}The simplification tactics}{63}`
`   139 \contentsline {section}{\numberline {8.2}The simplification tactics}{62}`
`   140 \contentsline {section}{\numberline {8.3}Example: using the simplifier}{64}`
`   140 \contentsline {section}{\numberline {8.3}Example: using the simplifier}{63}`
`   141 \contentsline {chapter}{\numberline {9}The classical theorem prover}{67}`
`   141 \contentsline {chapter}{\numberline {9}The classical theorem prover}{67}`
`   142 \contentsline {section}{\numberline {9.1}The sequent calculus}{67}`
`   142 \contentsline {section}{\numberline {9.1}The sequent calculus}{67}`
`   143 \contentsline {section}{\numberline {9.2}Simulating sequents by natural deduction}{68}`
`   143 \contentsline {section}{\numberline {9.2}Simulating sequents by natural deduction}{68}`
`   144 \contentsline {section}{\numberline {9.3}Extra rules for the sequent calculus}{69}`
`   144 \contentsline {section}{\numberline {9.3}Extra rules for the sequent calculus}{69}`
`   145 \contentsline {section}{\numberline {9.4}Classical rule sets}{70}`
`   145 \contentsline {section}{\numberline {9.4}Classical rule sets}{70}`