improved Makefile;
authorwenzelm
Wed May 05 18:35:41 1999 +0200 (1999-05-05)
changeset 66005a94bd71cc41
parent 6599 dc5bf3f40ad3
child 6601 51eed1aefccd
improved Makefile;
doc-src/Ref/Makefile
doc-src/Ref/ref.bbl
doc-src/Ref/ref.ind
doc-src/Ref/ref.rao
doc-src/System/Makefile
doc-src/System/system.ind
doc-src/Tutorial/Makefile
doc-src/Tutorial/tutorial.bbl
doc-src/Tutorial/tutorial.ind
     1.1 --- a/doc-src/Ref/Makefile	Wed May 05 18:26:10 1999 +0200
     1.2 +++ b/doc-src/Ref/Makefile	Wed May 05 18:35:41 1999 +0200
     1.3 @@ -1,35 +1,31 @@
     1.4 -#  $Id$
     1.5 -#########################################################################
     1.6 -#									#
     1.7 -#	Makefile for the report "The Isabelle Reference Manual"		#
     1.8 -#									#
     1.9 -#########################################################################
    1.10 +#
    1.11 +# $Id$
    1.12 +#
    1.13 +
    1.14 +## targets
    1.15 +
    1.16 +default: dvi
    1.17 +dist: dvi
    1.18  
    1.19  
    1.20 -FILES =  ref.tex introduction.tex goals.tex tactic.tex tctical.tex\
    1.21 -         thm.tex theories.tex defining.tex syntax.tex substitution.tex\
    1.22 -         simplifier.tex classical.tex theory-syntax.tex\
    1.23 -	 ../rail.sty ../proof.sty ../iman.sty ../extra.sty
    1.24 +## dependencies
    1.25 +
    1.26 +include ../Makefile.in
    1.27 +
    1.28 +NAME = ref
    1.29 +FILES = ref.tex introduction.tex goals.tex tactic.tex tctical.tex \
    1.30 +	thm.tex theories.tex defining.tex syntax.tex substitution.tex \
    1.31 +	simplifier.tex classical.tex theory-syntax.tex \
    1.32 +	../rail.sty ../proof.sty ../iman.sty ../extra.sty
    1.33  
    1.34 -ref.dvi.gz:   $(FILES) 
    1.35 -	test -r isabelle.eps || ln -s ../gfx/isabelle.eps .
    1.36 -	-rm ref.dvi*
    1.37 -	latex ref
    1.38 -	rail ref
    1.39 -	bibtex ref
    1.40 -	latex ref
    1.41 -	latex ref
    1.42 -	../sedindex ref
    1.43 -	latex ref
    1.44 -	gzip -f ref.dvi
    1.45 +dvi: $(NAME).dvi
    1.46  
    1.47 -dist:   $(FILES) 
    1.48 -	test -f isabelle.eps || ln -s ../gfx/isabelle.eps .
    1.49 -	rm -f ref.dvi*
    1.50 -	latex ref
    1.51 -	latex ref
    1.52 -	../sedindex ref
    1.53 -	latex ref
    1.54 -
    1.55 -clean:
    1.56 -	@rm *.aux *.log *.toc *.idx *.rai
    1.57 +$(NAME).dvi: $(FILES) isabelle.eps
    1.58 +	touch $(NAME).ind
    1.59 +	$(LATEX) $(NAME)
    1.60 +	$(RAIL) $(NAME)
    1.61 +	$(BIBTEX) $(NAME)
    1.62 +	$(LATEX) $(NAME)
    1.63 +	$(LATEX) $(NAME)
    1.64 +	$(SEDINDEX) $(NAME)
    1.65 +	$(LATEX) $(NAME)
     2.1 --- a/doc-src/Ref/ref.bbl	Wed May 05 18:26:10 1999 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,58 +0,0 @@
     2.4 -\begin{thebibliography}{10}
     2.5 -
     2.6 -\bibitem{bm88book}
     2.7 -Robert~S. Boyer and J~Strother Moore.
     2.8 -\newblock {\em A Computational Logic Handbook}.
     2.9 -\newblock Academic Press, 1988.
    2.10 -
    2.11 -\bibitem{charniak80}
    2.12 -E.~Charniak, C.~K. Riesbeck, and D.~V. McDermott.
    2.13 -\newblock {\em Artificial Intelligence Programming}.
    2.14 -\newblock Lawrence Erlbaum Associates, 1980.
    2.15 -
    2.16 -\bibitem{debruijn72}
    2.17 -N.~G. de~Bruijn.
    2.18 -\newblock Lambda calculus notation with nameless dummies, a tool for automatic
    2.19 -  formula manipulation, with application to the {Church-Rosser Theorem}.
    2.20 -\newblock {\em Indagationes Mathematicae}, 34:381--392, 1972.
    2.21 -
    2.22 -\bibitem{OBJ}
    2.23 -K.~Futatsugi, J.A. Goguen, Jean-Pierre Jouannaud, and J.~Meseguer.
    2.24 -\newblock Principles of {OBJ2}.
    2.25 -\newblock In {\em Symposium on Principles of Programming Languages}, pages
    2.26 -  52--66, 1985.
    2.27 -
    2.28 -\bibitem{martin-nipkow}
    2.29 -Ursula Martin and Tobias Nipkow.
    2.30 -\newblock Ordered rewriting and confluence.
    2.31 -\newblock In Mark~E. Stickel, editor, {\em 10th International Conference on
    2.32 -  Automated Deduction}, LNAI 449, pages 366--380. Springer, 1990.
    2.33 -
    2.34 -\bibitem{nipkow-patterns}
    2.35 -Tobias Nipkow.
    2.36 -\newblock Functional unification of higher-order patterns.
    2.37 -\newblock In M.~Vardi, editor, {\em Eighth Annual Symposium on Logic in
    2.38 -  Computer Science}, pages 64--74. {\sc ieee} Computer Society Press, 1993.
    2.39 -
    2.40 -\bibitem{nipkow-prehofer}
    2.41 -Tobias Nipkow and Christian Prehofer.
    2.42 -\newblock Type reconstruction for type classes.
    2.43 -\newblock {\em Journal of Functional Programming}, 5(2):201--224, 1995.
    2.44 -
    2.45 -\bibitem{nordstrom90}
    2.46 -Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith.
    2.47 -\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}.
    2.48 -\newblock Oxford University Press, 1990.
    2.49 -
    2.50 -\bibitem{paulson-ml2}
    2.51 -Lawrence~C. Paulson.
    2.52 -\newblock {\em {ML} for the Working Programmer}.
    2.53 -\newblock Cambridge University Press, 2nd edition, 1996.
    2.54 -
    2.55 -\bibitem{pelletier86}
    2.56 -F.~J. Pelletier.
    2.57 -\newblock Seventy-five problems for testing automatic theorem provers.
    2.58 -\newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.
    2.59 -\newblock Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135.
    2.60 -
    2.61 -\end{thebibliography}
     3.1 --- a/doc-src/Ref/ref.ind	Wed May 05 18:26:10 1999 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,904 +0,0 @@
     3.4 -\begin{theindex}
     3.5 -
     3.6 -  \item {\tt !!} symbol, 71
     3.7 -  \item {\tt\$}, \bold{62}, 88
     3.8 -  \item {\tt\%} symbol, 71
     3.9 -  \item * SplitterFun, 129
    3.10 -  \item {\tt ::} symbol, 71, 72
    3.11 -  \item {\tt ==} symbol, 71
    3.12 -  \item {\tt ==>} symbol, 71
    3.13 -  \item {\tt =>} symbol, 71
    3.14 -  \item {\tt =?=} symbol, 71
    3.15 -  \item {\tt\at Enum} constant, 94
    3.16 -  \item {\tt\at Finset} constant, 94, 95
    3.17 -  \item {\tt [} symbol, 71
    3.18 -  \item {\tt [|} symbol, 71
    3.19 -  \item {\tt \$ISABELLE_HOME}, 3
    3.20 -  \item {\tt ]} symbol, 71
    3.21 -  \item {\tt _K} constant, 96, 98
    3.22 -  \item \verb'{}' symbol, 94
    3.23 -  \item {\tt\ttlbrace} symbol, 71
    3.24 -  \item {\tt\ttrbrace} symbol, 71
    3.25 -  \item {\tt |]} symbol, 71
    3.26 -
    3.27 -  \indexspace
    3.28 -
    3.29 -  \item {\tt Abs}, \bold{62}, 88
    3.30 -  \item {\tt abstract_over}, \bold{63}
    3.31 -  \item {\tt abstract_rule}, \bold{49}
    3.32 -  \item {\tt aconv}, \bold{63}
    3.33 -  \item {\tt add_path}, \bold{60}
    3.34 -  \item {\tt addaltern}, \bold{137}
    3.35 -  \item {\tt addbefore}, \bold{137}
    3.36 -  \item {\tt Addcongs}, \bold{107}
    3.37 -  \item {\tt addcongs}, \bold{112}, 127, 128
    3.38 -  \item {\tt addD2}, \bold{136}
    3.39 -  \item {\tt AddDs}, \bold{142}
    3.40 -  \item {\tt addDs}, \bold{135}
    3.41 -  \item {\tt addE2}, \bold{136}
    3.42 -  \item {\tt addeqcongs}, \bold{112}, 128
    3.43 -  \item {\tt AddEs}, \bold{142}
    3.44 -  \item {\tt addEs}, \bold{135}
    3.45 -  \item {\tt AddIs}, \bold{142}
    3.46 -  \item {\tt addIs}, \bold{135}
    3.47 -  \item {\tt addloop}, \bold{114}
    3.48 -  \item {\tt addSaltern}, \bold{137}
    3.49 -  \item {\tt addSbefore}, \bold{137}
    3.50 -  \item {\tt addSD2}, \bold{136}
    3.51 -  \item {\tt AddSDs}, \bold{142}
    3.52 -  \item {\tt addSDs}, \bold{135}
    3.53 -  \item {\tt addSE2}, \bold{136}
    3.54 -  \item {\tt AddSEs}, \bold{142}
    3.55 -  \item {\tt addSEs}, \bold{135}
    3.56 -  \item {\tt Addsimprocs}, \bold{107}
    3.57 -  \item {\tt addsimprocs}, \bold{111}
    3.58 -  \item {\tt Addsimps}, \bold{107}
    3.59 -  \item {\tt addsimps}, \bold{110}, 128
    3.60 -  \item {\tt AddSIs}, \bold{142}
    3.61 -  \item {\tt addSIs}, \bold{135}
    3.62 -  \item {\tt addSolver}, \bold{113}
    3.63 -  \item {\tt Addsplits}, \bold{107}
    3.64 -  \item {\tt addsplits}, \bold{115}
    3.65 -  \item {\tt addss}, \bold{137}, 138
    3.66 -  \item {\tt addSSolver}, \bold{113}
    3.67 -  \item {\tt addSWrapper}, \bold{137}
    3.68 -  \item {\tt addWrapper}, \bold{137}
    3.69 -  \item {\tt all_tac}, \bold{34}
    3.70 -  \item {\tt ALLGOALS}, \bold{38}, 119, 122
    3.71 -  \item ambiguity
    3.72 -    \subitem of parsed expressions, 81
    3.73 -  \item {\tt ancestors_of}, \bold{61}
    3.74 -  \item {\tt any} nonterminal, \bold{70}
    3.75 -  \item {\tt APPEND}, \bold{32}, 34
    3.76 -  \item {\tt APPEND'}, 39
    3.77 -  \item {\tt Appl}, 85
    3.78 -  \item {\tt aprop} nonterminal, \bold{72}
    3.79 -  \item {\tt ares_tac}, \bold{23}
    3.80 -  \item {\tt args} nonterminal, 95
    3.81 -  \item {\tt Arith} theory, 121
    3.82 -  \item arities
    3.83 -    \subitem context conditions, 58
    3.84 -  \item {\tt Asm_full_simp_tac}, \bold{106}
    3.85 -  \item {\tt asm_full_simp_tac}, 26, \bold{116}, 120
    3.86 -  \item {\tt asm_full_simplify}, 116
    3.87 -  \item {\tt asm_rl} theorem, 25
    3.88 -  \item {\tt Asm_simp_tac}, \bold{105}, 118
    3.89 -  \item {\tt asm_simp_tac}, \bold{116}, 128
    3.90 -  \item {\tt asm_simplify}, 116
    3.91 -  \item associative-commutative operators, 121
    3.92 -  \item {\tt assume}, \bold{48}
    3.93 -  \item {\tt assume_ax}, 10, \bold{12}
    3.94 -  \item {\tt assume_tac}, \bold{21}, 134
    3.95 -  \item {\tt assumption}, \bold{51}
    3.96 -  \item assumptions
    3.97 -    \subitem contradictory, 142
    3.98 -    \subitem deleting, 26
    3.99 -    \subitem in simplification, 105, 114
   3.100 -    \subitem inserting, 23
   3.101 -    \subitem negated, 132
   3.102 -    \subitem of main goal, 9, 10, 12, 17, 18
   3.103 -    \subitem reordering, 120
   3.104 -    \subitem rotating, 26
   3.105 -    \subitem substitution in, 102
   3.106 -    \subitem tactics for, 21
   3.107 -  \item ASTs, 85--90
   3.108 -    \subitem made from parse trees, 86
   3.109 -    \subitem made from terms, 88
   3.110 -  \item {\tt atac}, \bold{23}
   3.111 -  \item {\tt Auto_tac}, \bold{142}
   3.112 -  \item {\tt auto_tac} $(cs,ss)$, \bold{139}
   3.113 -  \item {\tt axclass} section, 57
   3.114 -  \item axiomatic type class, 57
   3.115 -  \item axioms
   3.116 -    \subitem extracting, 11
   3.117 -  \item {\tt axioms_of}, \bold{11}
   3.118 -
   3.119 -  \indexspace
   3.120 -
   3.121 -  \item {\tt ba}, \bold{14}
   3.122 -  \item {\tt back}, \bold{13}
   3.123 -  \item batch execution, 16
   3.124 -  \item {\tt bd}, \bold{14}
   3.125 -  \item {\tt bds}, \bold{14}
   3.126 -  \item {\tt be}, \bold{14}
   3.127 -  \item {\tt bes}, \bold{14}
   3.128 -  \item {\tt BEST_FIRST}, \bold{35}, 36
   3.129 -  \item {\tt Best_tac}, \bold{142}
   3.130 -  \item {\tt best_tac}, \bold{140}
   3.131 -  \item {\tt beta_conversion}, \bold{49}
   3.132 -  \item {\tt bicompose}, \bold{52}
   3.133 -  \item {\tt bimatch_tac}, \bold{27}
   3.134 -  \item {\tt bind_thm}, \bold{11}, 12, 42
   3.135 -  \item binders, \bold{80}
   3.136 -  \item {\tt biresolution}, \bold{51}
   3.137 -  \item {\tt biresolve_tac}, \bold{27}, 143
   3.138 -  \item {\tt Blast.depth_tac}, \bold{139}
   3.139 -  \item {\tt Blast.trace}, \bold{139}
   3.140 -  \item {\tt Blast_tac}, \bold{142}
   3.141 -  \item {\tt blast_tac}, \bold{138}
   3.142 -  \item {\tt Bound}, \bold{62}, 86, 88, 89
   3.143 -  \item {\tt bound_hyp_subst_tac}, \bold{102}
   3.144 -  \item {\tt br}, \bold{14}
   3.145 -  \item {\tt BREADTH_FIRST}, \bold{35}
   3.146 -  \item {\tt brs}, \bold{14}
   3.147 -  \item {\tt bw}, \bold{15}
   3.148 -  \item {\tt bws}, \bold{15}
   3.149 -  \item {\tt by}, \bold{9}, 12--14, 18
   3.150 -  \item {\tt byev}, \bold{10}
   3.151 -
   3.152 -  \indexspace
   3.153 -
   3.154 -  \item {\tt cd}, \bold{3}
   3.155 -  \item {\tt cert_axm}, \bold{64}
   3.156 -  \item {\tt CHANGED}, \bold{34}
   3.157 -  \item {\tt chop}, \bold{12}, 17
   3.158 -  \item {\tt choplev}, \bold{13}
   3.159 -  \item {\tt Clarify_step_tac}, \bold{142}
   3.160 -  \item {\tt clarify_step_tac}, \bold{139}
   3.161 -  \item {\tt Clarify_tac}, \bold{142}
   3.162 -  \item {\tt clarify_tac}, \bold{139}
   3.163 -  \item {\tt Clarsimp_tac}, \bold{142}
   3.164 -  \item {\tt clarsimp_tac}, \bold{140}
   3.165 -  \item claset
   3.166 -    \subitem current, 141
   3.167 -  \item {\tt claset} ML type, 135
   3.168 -  \item {\tt ClasimpFun}, 144
   3.169 -  \item classes
   3.170 -    \subitem context conditions, 58
   3.171 -  \item classical reasoner, 130--144
   3.172 -    \subitem setting up, 143
   3.173 -    \subitem tactics, 138
   3.174 -  \item classical sets, 134
   3.175 -  \item {\tt ClassicalFun}, 143
   3.176 -  \item {\tt combination}, \bold{49}
   3.177 -  \item {\tt commit}, \bold{3}
   3.178 -  \item {\tt COMP}, \bold{51}
   3.179 -  \item {\tt compose}, \bold{51}
   3.180 -  \item {\tt compose_tac}, \bold{27}
   3.181 -  \item {\tt concl_of}, \bold{45}
   3.182 -  \item {\tt COND}, \bold{36}
   3.183 -  \item congruence rules, 111
   3.184 -  \item {\tt Const}, \bold{62}, 88, 98
   3.185 -  \item {\tt Constant}, 85, 98
   3.186 -  \item constants, \bold{62}
   3.187 -    \subitem for translations, 75
   3.188 -    \subitem syntactic, 90
   3.189 -  \item {\tt context}, \bold{4}, 105
   3.190 -  \item {\tt contr_tac}, \bold{142}
   3.191 -  \item {\tt could_unify}, \bold{29}
   3.192 -  \item {\tt cprems_of}, \bold{45}
   3.193 -  \item {\tt cprop_of}, \bold{44}
   3.194 -  \item {\tt CPure} theory, 55
   3.195 -  \item {\tt CPure.thy}, \bold{61}
   3.196 -  \item {\tt crep_thm}, \bold{45}
   3.197 -  \item {\tt cterm} ML type, 64
   3.198 -  \item {\tt cterm_instantiate}, \bold{43}
   3.199 -  \item {\tt cterm_of}, 9, 17, \bold{64}
   3.200 -  \item {\tt ctyp}, \bold{65}
   3.201 -  \item {\tt ctyp_of}, \bold{66}
   3.202 -  \item {\tt cut_facts_tac}, \bold{23}, 103
   3.203 -  \item {\tt cut_inst_tac}, \bold{23}
   3.204 -  \item {\tt cut_rl} theorem, 25
   3.205 -
   3.206 -  \indexspace
   3.207 -
   3.208 -  \item {\tt datatype}, 107
   3.209 -  \item {\tt Deepen_tac}, \bold{142}
   3.210 -  \item {\tt deepen_tac}, \bold{140}
   3.211 -  \item {\tt defer_tac}, \bold{24}
   3.212 -  \item definitions, \see{rewriting, meta-level}{1}, 24, \bold{58}
   3.213 -    \subitem unfolding, 9, 10
   3.214 -  \item {\tt del_path}, \bold{60}
   3.215 -  \item {\tt Delcongs}, \bold{107}
   3.216 -  \item {\tt delcongs}, \bold{112}
   3.217 -  \item {\tt deleqcongs}, \bold{112}
   3.218 -  \item {\tt delete_tmpfiles}, \bold{59}
   3.219 -  \item delimiters, \bold{72}, 75, 76, 78
   3.220 -  \item {\tt delloop}, \bold{114}
   3.221 -  \item {\tt delrules}, \bold{135}
   3.222 -  \item {\tt Delsimprocs}, \bold{107}
   3.223 -  \item {\tt delsimprocs}, \bold{111}
   3.224 -  \item {\tt Delsimps}, \bold{107}
   3.225 -  \item {\tt delsimps}, \bold{110}
   3.226 -  \item {\tt Delsplits}, \bold{107}
   3.227 -  \item {\tt delSWrapper}, \bold{137}
   3.228 -  \item {\tt delWrapper}, \bold{137}
   3.229 -  \item {\tt dependent_tr'}, 96, \bold{98}
   3.230 -  \item {\tt DEPTH_FIRST}, \bold{35}
   3.231 -  \item {\tt DEPTH_SOLVE}, \bold{35}
   3.232 -  \item {\tt DEPTH_SOLVE_1}, \bold{35}
   3.233 -  \item {\tt depth_tac}, \bold{140}
   3.234 -  \item {\tt Deriv.drop}, \bold{53}
   3.235 -  \item {\tt Deriv.linear}, \bold{53}
   3.236 -  \item {\tt Deriv.size}, \bold{53}
   3.237 -  \item {\tt Deriv.tree}, \bold{53}
   3.238 -  \item {\tt dest_eq}, \bold{103}
   3.239 -  \item {\tt dest_imp}, \bold{103}
   3.240 -  \item {\tt dest_state}, \bold{45}
   3.241 -  \item {\tt dest_Trueprop}, \bold{103}
   3.242 -  \item destruct-resolution, 21
   3.243 -  \item {\tt DETERM}, \bold{36}
   3.244 -  \item discrimination nets, \bold{28}
   3.245 -  \item {\tt distinct_subgoals_tac}, \bold{26}
   3.246 -  \item {\tt dmatch_tac}, \bold{21}
   3.247 -  \item {\tt domain_type}, \bold{104}
   3.248 -  \item {\tt dres_inst_tac}, \bold{22}
   3.249 -  \item {\tt dresolve_tac}, \bold{21}
   3.250 -  \item {\tt dtac}, \bold{23}
   3.251 -  \item {\tt dummyT}, 88, 89, 99
   3.252 -  \item duplicate subgoals
   3.253 -    \subitem removing, 26
   3.254 -
   3.255 -  \indexspace
   3.256 -
   3.257 -  \item elim-resolution, 20
   3.258 -  \item {\tt ematch_tac}, \bold{21}
   3.259 -  \item {\tt empty} constant, 94
   3.260 -  \item {\tt empty_cs}, \bold{135}
   3.261 -  \item {\tt empty_ss}, \bold{109}
   3.262 -  \item {\tt eq_assume_tac}, \bold{21}, 134
   3.263 -  \item {\tt eq_assumption}, \bold{51}
   3.264 -  \item {\tt eq_mp_tac}, \bold{142}
   3.265 -  \item {\tt eq_reflection} theorem, \bold{104}, 125
   3.266 -  \item {\tt eq_thm}, \bold{36}
   3.267 -  \item {\tt eq_thy}, \bold{60}
   3.268 -  \item {\tt equal_elim}, \bold{48}
   3.269 -  \item {\tt equal_intr}, \bold{48}
   3.270 -  \item equality, 101--104
   3.271 -  \item {\tt eres_inst_tac}, \bold{22}
   3.272 -  \item {\tt eresolve_tac}, \bold{20}
   3.273 -    \subitem on other than first premise, 44
   3.274 -  \item {\tt ERROR}, 6
   3.275 -  \item {\tt error}, 6
   3.276 -  \item error messages, 6
   3.277 -  \item {\tt eta_contract}, \bold{6}, 92
   3.278 -  \item {\tt etac}, \bold{23}
   3.279 -  \item {\tt EVERY}, \bold{33}
   3.280 -  \item {\tt EVERY'}, 39
   3.281 -  \item {\tt EVERY1}, \bold{40}
   3.282 -  \item examples
   3.283 -    \subitem of logic definitions, 82
   3.284 -    \subitem of macros, 94, 95
   3.285 -    \subitem of mixfix declarations, 77
   3.286 -    \subitem of simplification, 117
   3.287 -    \subitem of translations, 98
   3.288 -  \item exceptions
   3.289 -    \subitem printing of, 7
   3.290 -  \item {\tt exit}, \bold{3}
   3.291 -  \item {\tt extensional}, \bold{49}
   3.292 -
   3.293 -  \indexspace
   3.294 -
   3.295 -  \item {\tt fa}, \bold{15}
   3.296 -  \item {\tt Fast_tac}, \bold{142}
   3.297 -  \item {\tt fast_tac}, \bold{140}
   3.298 -  \item {\tt fd}, \bold{15}
   3.299 -  \item {\tt fds}, \bold{15}
   3.300 -  \item {\tt fe}, \bold{15}
   3.301 -  \item {\tt fes}, \bold{15}
   3.302 -  \item files
   3.303 -    \subitem reading, 3, 59
   3.304 -  \item {\tt filt_resolve_tac}, \bold{29}
   3.305 -  \item {\tt FILTER}, \bold{34}
   3.306 -  \item {\tt filter_goal}, \bold{19}
   3.307 -  \item {\tt filter_thms}, \bold{29}
   3.308 -  \item {\tt findE}, \bold{12}
   3.309 -  \item {\tt findEs}, \bold{12}
   3.310 -  \item {\tt findI}, \bold{12}
   3.311 -  \item {\tt FIRST}, \bold{33}
   3.312 -  \item {\tt FIRST'}, 39
   3.313 -  \item {\tt FIRST1}, \bold{40}
   3.314 -  \item {\tt FIRSTGOAL}, \bold{38}
   3.315 -  \item flex-flex constraints, 26, 44, 52
   3.316 -  \item {\tt flexflex_rule}, \bold{52}
   3.317 -  \item {\tt flexflex_tac}, \bold{26}
   3.318 -  \item {\tt FOL_basic_ss}, \bold{128}
   3.319 -  \item {\tt FOL_ss}, \bold{128}
   3.320 -  \item {\tt fold_goals_tac}, \bold{24}
   3.321 -  \item {\tt fold_tac}, \bold{24}
   3.322 -  \item {\tt forall_elim}, \bold{50}
   3.323 -  \item {\tt forall_elim_list}, \bold{50}
   3.324 -  \item {\tt forall_elim_var}, \bold{50}
   3.325 -  \item {\tt forall_elim_vars}, \bold{50}
   3.326 -  \item {\tt forall_intr}, \bold{49}
   3.327 -  \item {\tt forall_intr_frees}, \bold{50}
   3.328 -  \item {\tt forall_intr_list}, \bold{50}
   3.329 -  \item {\tt force_strip_shyps}, \bold{45}
   3.330 -  \item {\tt Force_tac}, \bold{142}
   3.331 -  \item {\tt force_tac}, \bold{139}
   3.332 -  \item {\tt forw_inst_tac}, \bold{22}
   3.333 -  \item forward proof, 21, 42
   3.334 -  \item {\tt forward_tac}, \bold{21}
   3.335 -  \item {\tt fr}, \bold{15}
   3.336 -  \item {\tt Free}, \bold{62}, 88
   3.337 -  \item {\tt freezeT}, \bold{50}
   3.338 -  \item {\tt frs}, \bold{15}
   3.339 -  \item {\tt Full_simp_tac}, \bold{105}
   3.340 -  \item {\tt full_simp_tac}, \bold{116}
   3.341 -  \item {\tt full_simplify}, 116
   3.342 -  \item {\textit {fun}} type, 65
   3.343 -  \item function applications, \bold{62}
   3.344 -
   3.345 -  \indexspace
   3.346 -
   3.347 -  \item {\tt get_axiom}, \bold{11}
   3.348 -  \item {\tt get_thm}, \bold{11}
   3.349 -  \item {\tt get_thms}, \bold{11}
   3.350 -  \item {\tt getenv}, 59
   3.351 -  \item {\tt getgoal}, \bold{18}
   3.352 -  \item {\tt gethyps}, \bold{19}, 38
   3.353 -  \item {\tt Goal}, \bold{9}, 17
   3.354 -  \item {\tt goal}, \bold{9}
   3.355 -  \item {\tt goals_limit}, \bold{13}
   3.356 -  \item {\tt Goalw}, \bold{9}
   3.357 -  \item {\tt goalw}, \bold{9}
   3.358 -  \item {\tt goalw_cterm}, \bold{9}
   3.359 -
   3.360 -  \indexspace
   3.361 -
   3.362 -  \item {\tt has_fewer_prems}, \bold{36}
   3.363 -  \item higher-order pattern, \bold{110}
   3.364 -  \item {\tt HOL_basic_ss}, \bold{109}
   3.365 -  \item {\tt hyp_subst_tac}, \bold{102}
   3.366 -  \item {\tt hyp_subst_tacs}, \bold{144}
   3.367 -  \item {\tt HypsubstFun}, 103, 144
   3.368 -
   3.369 -  \indexspace
   3.370 -
   3.371 -  \item {\tt id} nonterminal, \bold{72}, 86, 93
   3.372 -  \item identifiers, 72
   3.373 -  \item {\tt idt} nonterminal, 92
   3.374 -  \item {\tt idts} nonterminal, \bold{72}, 80
   3.375 -  \item {\tt IF_UNSOLVED}, \bold{36}
   3.376 -  \item {\tt iff_reflection} theorem, 125
   3.377 -  \item {\tt IFOL_ss}, \bold{128}
   3.378 -  \item {\tt imp_intr} theorem, \bold{104}
   3.379 -  \item {\tt implies_elim}, \bold{48}
   3.380 -  \item {\tt implies_elim_list}, \bold{48}
   3.381 -  \item {\tt implies_intr}, \bold{48}
   3.382 -  \item {\tt implies_intr_hyps}, \bold{48}
   3.383 -  \item {\tt implies_intr_list}, \bold{48}
   3.384 -  \item {\tt incr_boundvars}, \bold{63}, 98
   3.385 -  \item {\tt indexname} ML type, 62, 73
   3.386 -  \item infixes, \bold{79}
   3.387 -  \item {\tt insert} constant, 94
   3.388 -  \item {\tt inst_step_tac}, \bold{141}
   3.389 -  \item {\tt instance} section, 57
   3.390 -  \item {\tt instantiate}, \bold{50}
   3.391 -  \item {\tt instantiate'}, \bold{43}, 50
   3.392 -  \item instantiation, 22, 43, 50
   3.393 -  \item {\tt INTLEAVE}, \bold{32}, 34
   3.394 -  \item {\tt INTLEAVE'}, 39
   3.395 -  \item {\tt invoke_oracle}, \bold{66}
   3.396 -  \item {\tt is} nonterminal, 94
   3.397 -
   3.398 -  \indexspace
   3.399 -
   3.400 -  \item {\tt joinrules}, \bold{143}
   3.401 -
   3.402 -  \indexspace
   3.403 -
   3.404 -  \item {\tt keep_derivs}, \bold{53}
   3.405 -
   3.406 -  \indexspace
   3.407 -
   3.408 -  \item $\lambda$-abstractions, 28, \bold{62}
   3.409 -  \item $\lambda$-calculus, 47, 49, 72
   3.410 -  \item {\tt lessb}, \bold{28}
   3.411 -  \item lexer, \bold{72}
   3.412 -  \item {\tt lift_rule}, \bold{52}
   3.413 -  \item lifting, 52
   3.414 -  \item {\tt logic} class, 72, 77
   3.415 -  \item {\tt logic} nonterminal, \bold{72}
   3.416 -  \item {\tt Logic.auto_rename}, \bold{26}
   3.417 -  \item {\tt Logic.set_rename_prefix}, \bold{25}
   3.418 -  \item {\tt long_names}, \bold{6}
   3.419 -  \item {\tt loose_bnos}, \bold{63}, 99
   3.420 -
   3.421 -  \indexspace
   3.422 -
   3.423 -  \item macros, 90--96
   3.424 -  \item {\tt make_elim}, \bold{44}, 136
   3.425 -  \item {\tt Match} exception, 97
   3.426 -  \item {\tt match_tac}, \bold{21}, 134
   3.427 -  \item {\tt max_pri}, 70, \bold{76}
   3.428 -  \item {\tt merge_ss}, \bold{109}
   3.429 -  \item meta-assumptions, 37, 46, 48, 51
   3.430 -    \subitem printing of, 5
   3.431 -  \item meta-equality, 47--49
   3.432 -  \item meta-implication, 47, 48
   3.433 -  \item meta-quantifiers, 47, 49
   3.434 -  \item meta-rewriting, 9, 15, 16, \bold{24}, 
   3.435 -		\seealso{tactics, theorems}{145}
   3.436 -    \subitem in theorems, 43
   3.437 -  \item meta-rules, \see{meta-rules}{1}, 46--52
   3.438 -  \item {\tt METAHYPS}, 19, \bold{37}
   3.439 -  \item mixfix declarations, 57, 75--80
   3.440 -  \item {\tt mk_atomize}, \bold{127}
   3.441 -  \item {\tt mk_simproc}, \bold{123}
   3.442 -  \item {\tt ML} section, 58, 97, 99
   3.443 -  \item model checkers, 81
   3.444 -  \item {\tt mp} theorem, \bold{143}
   3.445 -  \item {\tt mp_tac}, \bold{142}
   3.446 -  \item {\tt MRL}, \bold{42}
   3.447 -  \item {\tt MRS}, \bold{42}
   3.448 -
   3.449 -  \indexspace
   3.450 -
   3.451 -  \item name tokens, \bold{72}
   3.452 -  \item {\tt nat_cancel}, \bold{111}
   3.453 -  \item {\tt net_bimatch_tac}, \bold{28}
   3.454 -  \item {\tt net_biresolve_tac}, \bold{28}
   3.455 -  \item {\tt net_match_tac}, \bold{28}
   3.456 -  \item {\tt net_resolve_tac}, \bold{28}
   3.457 -  \item {\tt no_tac}, \bold{34}
   3.458 -  \item {\tt None}, \bold{30}
   3.459 -  \item {\tt nonterminal} symbols, 56
   3.460 -  \item {\tt not_elim} theorem, \bold{143}
   3.461 -  \item {\tt nprems_of}, \bold{45}
   3.462 -  \item numerals, 72
   3.463 -
   3.464 -  \indexspace
   3.465 -
   3.466 -  \item {\textit {o}} type, 82
   3.467 -  \item {\tt object}, 66
   3.468 -  \item {\tt op} symbol, 79
   3.469 -  \item {\tt option} ML type, 30
   3.470 -  \item oracles, 66--68
   3.471 -  \item {\tt ORELSE}, \bold{32}, 34, 38
   3.472 -  \item {\tt ORELSE'}, 39
   3.473 -
   3.474 -  \indexspace
   3.475 -
   3.476 -  \item parameters
   3.477 -    \subitem removing unused, 26
   3.478 -    \subitem renaming, 15, 25, 52
   3.479 -  \item {\tt parents_of}, \bold{61}
   3.480 -  \item parse trees, 85
   3.481 -  \item {\tt parse_rules}, 92
   3.482 -  \item pattern, higher-order, \bold{110}
   3.483 -  \item {\tt pause_tac}, \bold{30}
   3.484 -  \item Poly/{\ML} compiler, 7
   3.485 -  \item {\tt pop_proof}, \bold{17}
   3.486 -  \item {\tt pr}, \bold{13}
   3.487 -  \item {\tt premises}, \bold{9}, 17
   3.488 -  \item {\tt prems_of}, \bold{45}
   3.489 -  \item {\tt prems_of_ss}, \bold{113}
   3.490 -  \item pretty printing, 76, 78--79, 95
   3.491 -  \item {\tt Pretty.setdepth}, \bold{5}
   3.492 -  \item {\tt Pretty.setmargin}, \bold{5}
   3.493 -  \item {\tt PRIMITIVE}, \bold{29}
   3.494 -  \item {\tt primrec}, 107
   3.495 -  \item {\tt prin}, 7, \bold{18}
   3.496 -  \item print mode, 56, 99
   3.497 -  \item print modes, 80--81
   3.498 -  \item {\tt print_cs}, \bold{135}
   3.499 -  \item {\tt print_depth}, \bold{5}
   3.500 -  \item {\tt print_exn}, \bold{7}, 41
   3.501 -  \item {\tt print_goals}, \bold{42}
   3.502 -  \item {\tt print_mode}, 80
   3.503 -  \item {\tt print_modes}, 75
   3.504 -  \item {\tt print_rules}, 92
   3.505 -  \item {\tt print_simpset}, \bold{109}
   3.506 -  \item {\tt print_ss}, \bold{108}
   3.507 -  \item {\tt print_syntax}, \bold{61}, \bold{74}
   3.508 -  \item {\tt print_tac}, \bold{30}
   3.509 -  \item {\tt print_theory}, \bold{61}
   3.510 -  \item {\tt print_thm}, \bold{42}
   3.511 -  \item printing control, 4--6
   3.512 -  \item {\tt printyp}, \bold{18}
   3.513 -  \item priorities, 69, \bold{76}
   3.514 -  \item priority grammars, 69--70
   3.515 -  \item {\tt prlev}, \bold{13}
   3.516 -  \item {\tt prlim}, \bold{13}
   3.517 -  \item productions, 69, 75, 76
   3.518 -    \subitem copy, \bold{75}, 76, 87
   3.519 -  \item {\tt proof} ML type, 18
   3.520 -  \item proof objects, 52--54
   3.521 -  \item proof state, 8
   3.522 -    \subitem printing of, 13
   3.523 -  \item {\tt proof_timing}, \bold{14}
   3.524 -  \item proofs, 8--19
   3.525 -    \subitem inspecting the state, 18
   3.526 -    \subitem managing multiple, 17
   3.527 -    \subitem saving and restoring, 18
   3.528 -    \subitem stacking, 17
   3.529 -    \subitem starting, 8
   3.530 -    \subitem timing, 14
   3.531 -  \item {\tt PROP} symbol, 71
   3.532 -  \item {\textit {prop}} type, 65, 72
   3.533 -  \item {\tt prop} nonterminal, \bold{70}, 82
   3.534 -  \item {\tt ProtoPure.thy}, \bold{61}
   3.535 -  \item {\tt prove_goal}, 14, \bold{16}
   3.536 -  \item {\tt prove_goalw}, \bold{16}
   3.537 -  \item {\tt prove_goalw_cterm}, \bold{16}
   3.538 -  \item {\tt prth}, \bold{41}
   3.539 -  \item {\tt prthq}, \bold{42}
   3.540 -  \item {\tt prths}, \bold{42}
   3.541 -  \item {\tt prune_params_tac}, \bold{26}
   3.542 -  \item {\tt pttrn} nonterminal, \bold{72}
   3.543 -  \item {\tt pttrns} nonterminal, \bold{72}
   3.544 -  \item {\tt Pure} theory, 55, 70, 74
   3.545 -  \item {\tt Pure.thy}, \bold{61}
   3.546 -  \item {\tt push_proof}, \bold{17}
   3.547 -  \item {\tt pwd}, \bold{3}
   3.548 -
   3.549 -  \indexspace
   3.550 -
   3.551 -  \item {\tt qed}, \bold{10}, 12
   3.552 -  \item {\tt qed_goal}, \bold{16}
   3.553 -  \item {\tt qed_goalw}, \bold{16}
   3.554 -  \item quantifiers, 80
   3.555 -  \item {\tt quit}, \bold{3}
   3.556 -
   3.557 -  \indexspace
   3.558 -
   3.559 -  \item {\tt read}, \bold{18}
   3.560 -  \item {\tt read_axm}, \bold{64}
   3.561 -  \item {\tt read_cterm}, \bold{64}
   3.562 -  \item {\tt read_instantiate}, \bold{43}
   3.563 -  \item {\tt read_instantiate_sg}, \bold{43}
   3.564 -  \item reading
   3.565 -    \subitem axioms, \see{{\tt assume_ax}}{55}
   3.566 -    \subitem goals, \see{proofs, starting}{8}
   3.567 -  \item {\tt reflexive}, \bold{49}
   3.568 -  \item {\tt ren}, \bold{15}
   3.569 -  \item {\tt rename_last_tac}, \bold{25}
   3.570 -  \item {\tt rename_params_rule}, \bold{52}
   3.571 -  \item {\tt rename_tac}, \bold{25}
   3.572 -  \item {\tt rep_cs}, \bold{135}
   3.573 -  \item {\tt rep_cterm}, \bold{64}
   3.574 -  \item {\tt rep_ctyp}, \bold{66}
   3.575 -  \item {\tt rep_ss}, \bold{108}
   3.576 -  \item {\tt rep_thm}, \bold{45}
   3.577 -  \item {\tt REPEAT}, \bold{33, 34}
   3.578 -  \item {\tt REPEAT1}, \bold{33}
   3.579 -  \item {\tt REPEAT_DETERM}, \bold{33}
   3.580 -  \item {\tt REPEAT_FIRST}, \bold{39}
   3.581 -  \item {\tt REPEAT_SOME}, \bold{38}
   3.582 -  \item {\tt res_inst_tac}, \bold{22}, 26, 27
   3.583 -  \item reserved words, 72, 95
   3.584 -  \item {\tt reset}, 4
   3.585 -  \item {\tt reset_path}, \bold{60}
   3.586 -  \item resolution, 42, 51
   3.587 -    \subitem tactics, 20
   3.588 -    \subitem without lifting, 51
   3.589 -  \item {\tt resolve_tac}, \bold{20}, 134
   3.590 -  \item {\tt restore_proof}, \bold{18}
   3.591 -  \item {\tt result}, \bold{10}, 12, 18
   3.592 -  \item {\tt rev_mp} theorem, \bold{104}
   3.593 -  \item rewrite rules, 110
   3.594 -    \subitem permutative, 120--123
   3.595 -  \item {\tt rewrite_goals_rule}, \bold{43}
   3.596 -  \item {\tt rewrite_goals_tac}, \bold{24}, 43
   3.597 -  \item {\tt rewrite_rule}, \bold{43}
   3.598 -  \item {\tt rewrite_tac}, 10, \bold{24}
   3.599 -  \item rewriting
   3.600 -    \subitem object-level, \see{simplification}{1}
   3.601 -    \subitem ordered, 121
   3.602 -    \subitem syntactic, 90--96
   3.603 -  \item {\tt rewtac}, \bold{23}
   3.604 -  \item {\tt RL}, \bold{42}
   3.605 -  \item {\tt RLN}, \bold{42}
   3.606 -  \item {\tt rotate_prems}, \bold{44}
   3.607 -  \item {\tt rotate_proof}, \bold{17}
   3.608 -  \item {\tt rotate_tac}, \bold{26}
   3.609 -  \item {\tt RS}, \bold{42}
   3.610 -  \item {\tt RSN}, \bold{42}
   3.611 -  \item {\tt rtac}, \bold{23}
   3.612 -  \item {\tt rule_by_tactic}, 26, \bold{44}
   3.613 -  \item rules
   3.614 -    \subitem converting destruction to elimination, 44
   3.615 -
   3.616 -  \indexspace
   3.617 -
   3.618 -  \item {\tt safe_asm_full_simp_tac}, \bold{116}
   3.619 -  \item {\tt Safe_step_tac}, \bold{142}
   3.620 -  \item {\tt safe_step_tac}, 136, \bold{141}
   3.621 -  \item {\tt Safe_tac}, \bold{142}
   3.622 -  \item {\tt safe_tac}, \bold{141}
   3.623 -  \item {\tt save_proof}, \bold{18}
   3.624 -  \item saving your session, \bold{2}
   3.625 -  \item search, 32
   3.626 -    \subitem tacticals, 34--36
   3.627 -  \item {\tt SELECT_GOAL}, 24, \bold{37}
   3.628 -  \item {\tt Seq.seq} ML type, 29
   3.629 -  \item sequences (lazy lists), \bold{30}
   3.630 -  \item sequent calculus, 131
   3.631 -  \item sessions, 1--7
   3.632 -  \item {\tt set}, 4
   3.633 -  \item {\tt setloop}, \bold{114}
   3.634 -  \item {\tt setmksimps}, 110, \bold{126}, 128
   3.635 -  \item {\tt setSolver}, \bold{113}, 128
   3.636 -  \item {\tt setSSolver}, \bold{113}, 128
   3.637 -  \item {\tt setsubgoaler}, \bold{112}, 128
   3.638 -  \item {\tt settermless}, \bold{121}
   3.639 -  \item {\tt setup}
   3.640 -    \subitem simplifier, 129
   3.641 -    \subitem theory, 58
   3.642 -  \item shortcuts
   3.643 -    \subitem for \texttt{by} commands, 14
   3.644 -    \subitem for tactics, 23
   3.645 -  \item {\tt show_brackets}, \bold{5}
   3.646 -  \item {\tt show_consts}, \bold{6}
   3.647 -  \item {\tt show_hyps}, \bold{5}
   3.648 -  \item {\tt show_path}, \bold{60}
   3.649 -  \item {\tt show_sorts}, \bold{5}, 89, 97
   3.650 -  \item {\tt show_tags}, \bold{5}
   3.651 -  \item {\tt show_types}, \bold{5}, 89, 92, 99
   3.652 -  \item {\tt Sign.certify_term}, \bold{64}
   3.653 -  \item {\tt Sign.certify_typ}, \bold{66}
   3.654 -  \item {\tt Sign.sg} ML type, 55
   3.655 -  \item {\tt Sign.stamp_names_of}, \bold{61}
   3.656 -  \item {\tt Sign.string_of_term}, \bold{64}
   3.657 -  \item {\tt Sign.string_of_typ}, \bold{65}
   3.658 -  \item {\tt sign_of}, 9, 17, \bold{61}
   3.659 -  \item {\tt sign_of_thm}, \bold{45}
   3.660 -  \item signatures, \bold{55}, 61, 63, 64, 66
   3.661 -  \item {\tt Simp_tac}, \bold{105}
   3.662 -  \item {\tt simp_tac}, \bold{116}
   3.663 -  \item simplification, 105--129
   3.664 -    \subitem conversions, 116
   3.665 -    \subitem forward rules, 116
   3.666 -    \subitem from classical reasoner, 137
   3.667 -    \subitem setting up, 125
   3.668 -    \subitem setting up the splitter, 129
   3.669 -    \subitem setting up the theory, 129
   3.670 -    \subitem tactics, 115
   3.671 -  \item simplification sets, 108
   3.672 -  \item {\tt Simplifier.asm_full_rewrite}, 116
   3.673 -  \item {\tt Simplifier.asm_rewrite}, 116
   3.674 -  \item {\tt Simplifier.full_rewrite}, 116
   3.675 -  \item {\tt Simplifier.rewrite}, 116
   3.676 -  \item {\tt Simplifier.setup}, \bold{129}
   3.677 -  \item {\tt simplify}, 116
   3.678 -  \item {\tt SIMPSET}, \bold{109}
   3.679 -  \item simpset
   3.680 -    \subitem current, 105, 109
   3.681 -  \item {\tt simpset}, \bold{109}
   3.682 -  \item {\tt SIMPSET'}, \bold{109}
   3.683 -  \item {\tt simpset_of}, \bold{109}
   3.684 -  \item {\tt simpset_ref}, \bold{109}
   3.685 -  \item {\tt simpset_ref_of}, \bold{109}
   3.686 -  \item {\tt size_of_thm}, 35, \bold{36}, 143
   3.687 -  \item {\tt sizef}, \bold{143}
   3.688 -  \item {\tt slow_best_tac}, \bold{140}
   3.689 -  \item {\tt slow_step_tac}, 136, \bold{141}
   3.690 -  \item {\tt slow_tac}, \bold{140}
   3.691 -  \item {\tt SOLVE}, \bold{36}
   3.692 -  \item {\tt Some}, \bold{30}
   3.693 -  \item {\tt SOMEGOAL}, \bold{38}
   3.694 -  \item {\tt sort} nonterminal, \bold{72}
   3.695 -  \item sort constraints, 71
   3.696 -  \item sort hypotheses, 45, 47
   3.697 -  \item sorts
   3.698 -    \subitem printing of, 5
   3.699 -  \item {\tt ssubst} theorem, \bold{101}
   3.700 -  \item {\tt stac}, \bold{102}
   3.701 -  \item stamps, \bold{55}, 61
   3.702 -  \item {\tt standard}, \bold{44}
   3.703 -  \item starting up, \bold{1}
   3.704 -  \item {\tt Step_tac}, \bold{142}
   3.705 -  \item {\tt step_tac}, 136, \bold{141}
   3.706 -  \item {\tt store_thm}, \bold{11}
   3.707 -  \item {\tt string_of_cterm}, \bold{64}
   3.708 -  \item {\tt string_of_ctyp}, \bold{65}
   3.709 -  \item {\tt string_of_thm}, \bold{42}
   3.710 -  \item strings, 72
   3.711 -  \item {\tt SUBGOAL}, \bold{29}
   3.712 -  \item subgoal module, 8--19
   3.713 -  \item {\tt subgoal_tac}, \bold{23}
   3.714 -  \item {\tt subgoals_of_brl}, \bold{27}
   3.715 -  \item {\tt subgoals_tac}, \bold{24}
   3.716 -  \item {\tt subst} theorem, 101, \bold{104}
   3.717 -  \item substitution
   3.718 -    \subitem rules, 101
   3.719 -  \item {\tt subthy}, \bold{60}
   3.720 -  \item {\tt swap} theorem, \bold{143}
   3.721 -  \item {\tt swap_res_tac}, \bold{143}
   3.722 -  \item {\tt swapify}, \bold{143}
   3.723 -  \item {\tt sym} theorem, 102, \bold{104}
   3.724 -  \item {\tt symmetric}, \bold{49}
   3.725 -  \item {\tt syn_of}, \bold{74}
   3.726 -  \item syntax
   3.727 -    \subitem Pure, 70--75
   3.728 -    \subitem transformations, 85--99
   3.729 -  \item {\tt syntax} section, 56
   3.730 -  \item {\tt Syntax.ast} ML type, 85
   3.731 -  \item {\tt Syntax.mark_boundT}, 99
   3.732 -  \item {\tt Syntax.print_gram}, \bold{74}
   3.733 -  \item {\tt Syntax.print_syntax}, \bold{74}
   3.734 -  \item {\tt Syntax.print_trans}, \bold{74}
   3.735 -  \item {\tt Syntax.stat_norm_ast}, 94
   3.736 -  \item {\tt Syntax.syntax} ML type, 74
   3.737 -  \item {\tt Syntax.test_read}, 78, 94
   3.738 -  \item {\tt Syntax.trace_norm_ast}, 94
   3.739 -  \item {\tt Syntax.variant_abs'}, 99
   3.740 -
   3.741 -  \indexspace
   3.742 -
   3.743 -  \item {\tt tactic} ML type, 20
   3.744 -  \item tacticals, 32--40
   3.745 -    \subitem conditional, 36
   3.746 -    \subitem deterministic, 36
   3.747 -    \subitem for filtering, 34
   3.748 -    \subitem for restriction to a subgoal, 37
   3.749 -    \subitem identities for, 33
   3.750 -    \subitem joining a list of tactics, 33
   3.751 -    \subitem joining tactic functions, 39
   3.752 -    \subitem joining two tactics, 32
   3.753 -    \subitem repetition, 33
   3.754 -    \subitem scanning for subgoals, 38
   3.755 -    \subitem searching, 35
   3.756 -  \item tactics, 20--31
   3.757 -    \subitem assumption, \bold{21}, 23
   3.758 -    \subitem commands for applying, 9
   3.759 -    \subitem debugging, 18
   3.760 -    \subitem filtering results of, 34
   3.761 -    \subitem for composition, 27
   3.762 -    \subitem for contradiction, 142
   3.763 -    \subitem for inserting facts, 23
   3.764 -    \subitem for Modus Ponens, 142
   3.765 -    \subitem instantiation, 22
   3.766 -    \subitem matching, 21
   3.767 -    \subitem meta-rewriting, 23, \bold{24}
   3.768 -    \subitem primitives for coding, 29
   3.769 -    \subitem resolution, \bold{20}, 23, 27, 28
   3.770 -    \subitem restricting to a subgoal, 37
   3.771 -    \subitem simplification, 115
   3.772 -    \subitem substitution, 101--104
   3.773 -    \subitem tracing, 30
   3.774 -  \item {\tt TERM}, 64
   3.775 -  \item {\tt term} ML type, 62, 88
   3.776 -  \item terms, \bold{62}
   3.777 -    \subitem certified, \bold{63}
   3.778 -    \subitem made from ASTs, 88
   3.779 -    \subitem printing of, 18, 64
   3.780 -    \subitem reading of, 18
   3.781 -  \item {\tt TFree}, \bold{65}
   3.782 -  \item {\tt the_context}, \bold{4}
   3.783 -  \item {\tt THEN}, \bold{32}, 34, 38
   3.784 -  \item {\tt THEN'}, 39
   3.785 -  \item {\tt THEN_BEST_FIRST}, \bold{35}
   3.786 -  \item theorems, 41--54
   3.787 -    \subitem equality of, 36
   3.788 -    \subitem extracting, 11
   3.789 -    \subitem extracting proved, 10
   3.790 -    \subitem joining by resolution, 42
   3.791 -    \subitem of pure theory, 25
   3.792 -    \subitem printing of, 41
   3.793 -    \subitem retrieving, 12
   3.794 -    \subitem size of, 36
   3.795 -    \subitem standardizing, 44
   3.796 -    \subitem storing, 11
   3.797 -    \subitem taking apart, 44
   3.798 -  \item theories, 55--68
   3.799 -    \subitem axioms of, 11
   3.800 -    \subitem inspecting, \bold{61}
   3.801 -    \subitem parent, \bold{55}
   3.802 -    \subitem reading, 3, 59
   3.803 -    \subitem theorems of, 11
   3.804 -  \item {\tt THEORY} exception, 11, 55
   3.805 -  \item {\tt theory}, \bold{4}
   3.806 -  \item {\tt theory} ML type, 55
   3.807 -  \item {\tt Theory.add_oracle}, \bold{66}
   3.808 -  \item {\tt theory_of_thm}, \bold{45}
   3.809 -  \item {\tt thin_refl} theorem, \bold{104}
   3.810 -  \item {\tt thin_tac}, \bold{26}
   3.811 -  \item {\tt THM} exception, 41, 42, 46, 51
   3.812 -  \item {\tt thm}, \bold{11}
   3.813 -  \item {\tt thm} ML type, 41
   3.814 -  \item {\tt thms}, \bold{11}
   3.815 -  \item {\tt thms_containing}, \bold{12}
   3.816 -  \item {\tt thms_of}, \bold{11}
   3.817 -  \item {\tt tid} nonterminal, \bold{72}, 86, 93
   3.818 -  \item {\tt time_use}, \bold{3}
   3.819 -  \item {\tt time_use_thy}, \bold{4}
   3.820 -  \item timing statistics, 14
   3.821 -  \item {\tt toggle}, 4
   3.822 -  \item token class, 99
   3.823 -  \item token translations, 99--100
   3.824 -  \item token_translation, 100
   3.825 -  \item {\tt token_translation}, 100
   3.826 -  \item {\tt topthm}, \bold{18}
   3.827 -  \item {\tt touch_thy}, \bold{59}
   3.828 -  \item {\tt tpairs_of}, \bold{45}
   3.829 -  \item {\tt trace_BEST_FIRST}, \bold{35}
   3.830 -  \item {\tt trace_DEPTH_FIRST}, \bold{35}
   3.831 -  \item {\tt trace_goalno_tac}, \bold{39}
   3.832 -  \item {\tt trace_REPEAT}, \bold{33}
   3.833 -  \item {\tt trace_simp}, \bold{106}, 118
   3.834 -  \item tracing
   3.835 -    \subitem of classical prover, 139
   3.836 -    \subitem of macros, 94
   3.837 -    \subitem of searching tacticals, 35
   3.838 -    \subitem of simplification, 107, 118--119
   3.839 -    \subitem of tactics, 30
   3.840 -    \subitem of unification, 46
   3.841 -  \item {\tt transfer}, \bold{60}
   3.842 -  \item {\tt transfer_sg}, \bold{61}
   3.843 -  \item {\tt transitive}, \bold{49}
   3.844 -  \item translations, 96--99
   3.845 -    \subitem parse, 80, 88
   3.846 -    \subitem parse AST, \bold{86}, 87
   3.847 -    \subitem print, 80
   3.848 -    \subitem print AST, \bold{89}
   3.849 -  \item {\tt translations} section, 91
   3.850 -  \item {\tt trivial}, \bold{52}
   3.851 -  \item {\tt Trueprop} constant, 82
   3.852 -  \item {\tt TRY}, \bold{33, 34}
   3.853 -  \item {\tt TRYALL}, \bold{38}
   3.854 -  \item {\tt TVar}, \bold{65}
   3.855 -  \item {\tt tvar} nonterminal, \bold{72, 73}, 86, 93
   3.856 -  \item {\tt typ} ML type, 65
   3.857 -  \item {\tt Type}, \bold{65}
   3.858 -  \item {\textit {type}} type, 77
   3.859 -  \item {\tt type} nonterminal, \bold{72}
   3.860 -  \item type constraints, 72, 80, 89
   3.861 -  \item type constructors, \bold{65}
   3.862 -  \item type identifiers, 72
   3.863 -  \item type synonyms, \bold{56}
   3.864 -  \item type unknowns, \bold{65}, 72
   3.865 -    \subitem freezing/thawing of, 50
   3.866 -  \item type variables, \bold{65}
   3.867 -  \item types, \bold{65}
   3.868 -    \subitem certified, \bold{65}
   3.869 -    \subitem printing of, 5, 18, 65
   3.870 -
   3.871 -  \indexspace
   3.872 -
   3.873 -  \item {\tt undo}, 8, \bold{13}, 17
   3.874 -  \item unknowns, \bold{62}, 72
   3.875 -  \item {\tt update_thy}, \bold{59}
   3.876 -  \item {\tt uresult}, \bold{10}, 12, 18
   3.877 -  \item {\tt use}, \bold{3}
   3.878 -  \item {\tt use_thy}, \bold{4}
   3.879 -  \item {\tt use_thy_only}, \bold{59}
   3.880 -
   3.881 -  \indexspace
   3.882 -
   3.883 -  \item {\tt Var}, \bold{62}, 88
   3.884 -  \item {\tt var} nonterminal, \bold{72, 73}, 86, 93
   3.885 -  \item {\tt Variable}, 85
   3.886 -  \item variables
   3.887 -    \subitem bound, \bold{62}
   3.888 -    \subitem free, \bold{62}
   3.889 -  \item {\tt variant_abs}, \bold{63}
   3.890 -  \item {\tt varifyT}, \bold{50}
   3.891 -
   3.892 -  \indexspace
   3.893 -
   3.894 -  \item {\tt warning}, 6
   3.895 -  \item warnings, 6
   3.896 -  \item {\tt writeln}, 6
   3.897 -
   3.898 -  \indexspace
   3.899 -
   3.900 -  \item {\tt xnum} nonterminal, \bold{72}, 86, 93
   3.901 -  \item {\tt xstr} nonterminal, \bold{72}, 86, 93
   3.902 -
   3.903 -  \indexspace
   3.904 -
   3.905 -  \item {\tt zero_var_indexes}, \bold{44}
   3.906 -
   3.907 -\end{theindex}
     4.1 --- a/doc-src/Ref/ref.rao	Wed May 05 18:26:10 1999 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,449 +0,0 @@
     4.4 -% This file was generated by 'rail' from 'ref.rai'
     4.5 -\rail@t {lbrace}
     4.6 -\rail@t {rbrace}
     4.7 -\rail@i {1}{ \par theoryDef : id '=' (name + '+') ('+' extension | ()) ; \par name : id | string ; \par extension : (section +) 'end' ( () | ml ) ; \par section : classes | default | types | arities | nonterminals | consts | syntax | trans | defs | constdefs | rules | axclass | instance | oracle | local | global | setup ; \par classes : 'classes' ( classDecl + ) ; \par classDecl : (id (() | '<' (id + ','))) ; \par default : 'default' sort ; \par sort : id | lbrace (id * ',') rbrace ; \par types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + ) ; \par infix : ( 'infixr' | 'infixl' ) (() | string) nat ; \par typeDecl : typevarlist name ( () | '=' ( string | type ) ); \par typevarlist : () | tid | '(' ( tid + ',' ) ')'; \par type : simpleType | '(' type ')' | type '=>' type | '[' ( type + "," ) ']' '=>' type; \par simpleType: id | ( tid ( () | '::' id ) ) | '(' ( type + "," ) ')' id | simpleType id ; \par arities : 'arities' ((name + ',') '::' arity +) ; \par arity : ( () | '(' (sort + ',') ')' ) sort ; \par nonterminals : 'nonterminals' (name+) ; \par consts : 'consts' ( mixfixConstDecl + ) ; \par syntax : 'syntax' (() | mode) ( mixfixConstDecl + ); \par mode : '(' name (() | 'output') ')' ; \par mixfixConstDecl : constDecl (() | ( '(' mixfix ')' )) ; \par constDecl : ( name + ',') '::' (string | type); \par mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat ) | infix | 'binder' string nat ; \par trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + ) ; \par pat : ( () | ( '(' id ')' ) ) string; \par rules : 'rules' (( id string ) + ) ; \par defs : 'defs' (( id string ) + ) ; \par constdefs : 'constdefs' (name '::' (string | type) (() | mixfix) string +) ; \par axclass : 'axclass' classDecl (() | ( id string ) +) ; \par instance : 'instance' ( name '<' name | name '::' arity) witness ; \par witness : (() | '(' ((string | id | longident) + ',') ')') (() | verbatim) ; \par oracle : 'oracle' name '=' name ; \par local : 'local' ; \par global : 'global' ; \par setup : 'setup' (id | longident) ; \par ml : 'ML' text ; \par }
     4.8 -\rail@o {1}{
     4.9 -\rail@begin{2}{theoryDef}
    4.10 -\rail@nont{id}[]
    4.11 -\rail@term{=}[]
    4.12 -\rail@plus
    4.13 -\rail@nont{name}[]
    4.14 -\rail@nextplus{1}
    4.15 -\rail@cterm{+}[]
    4.16 -\rail@endplus
    4.17 -\rail@bar
    4.18 -\rail@term{+}[]
    4.19 -\rail@nont{extension}[]
    4.20 -\rail@nextbar{1}
    4.21 -\rail@endbar
    4.22 -\rail@end
    4.23 -\rail@begin{2}{name}
    4.24 -\rail@bar
    4.25 -\rail@nont{id}[]
    4.26 -\rail@nextbar{1}
    4.27 -\rail@nont{string}[]
    4.28 -\rail@endbar
    4.29 -\rail@end
    4.30 -\rail@begin{2}{extension}
    4.31 -\rail@plus
    4.32 -\rail@nont{section}[]
    4.33 -\rail@nextplus{1}
    4.34 -\rail@endplus
    4.35 -\rail@term{end}[]
    4.36 -\rail@bar
    4.37 -\rail@nextbar{1}
    4.38 -\rail@nont{ml}[]
    4.39 -\rail@endbar
    4.40 -\rail@end
    4.41 -\rail@begin{17}{section}
    4.42 -\rail@bar
    4.43 -\rail@nont{classes}[]
    4.44 -\rail@nextbar{1}
    4.45 -\rail@nont{default}[]
    4.46 -\rail@nextbar{2}
    4.47 -\rail@nont{types}[]
    4.48 -\rail@nextbar{3}
    4.49 -\rail@nont{arities}[]
    4.50 -\rail@nextbar{4}
    4.51 -\rail@nont{nonterminals}[]
    4.52 -\rail@nextbar{5}
    4.53 -\rail@nont{consts}[]
    4.54 -\rail@nextbar{6}
    4.55 -\rail@nont{syntax}[]
    4.56 -\rail@nextbar{7}
    4.57 -\rail@nont{trans}[]
    4.58 -\rail@nextbar{8}
    4.59 -\rail@nont{defs}[]
    4.60 -\rail@nextbar{9}
    4.61 -\rail@nont{constdefs}[]
    4.62 -\rail@nextbar{10}
    4.63 -\rail@nont{rules}[]
    4.64 -\rail@nextbar{11}
    4.65 -\rail@nont{axclass}[]
    4.66 -\rail@nextbar{12}
    4.67 -\rail@nont{instance}[]
    4.68 -\rail@nextbar{13}
    4.69 -\rail@nont{oracle}[]
    4.70 -\rail@nextbar{14}
    4.71 -\rail@nont{local}[]
    4.72 -\rail@nextbar{15}
    4.73 -\rail@nont{global}[]
    4.74 -\rail@nextbar{16}
    4.75 -\rail@nont{setup}[]
    4.76 -\rail@endbar
    4.77 -\rail@end
    4.78 -\rail@begin{2}{classes}
    4.79 -\rail@term{classes}[]
    4.80 -\rail@plus
    4.81 -\rail@nont{classDecl}[]
    4.82 -\rail@nextplus{1}
    4.83 -\rail@endplus
    4.84 -\rail@end
    4.85 -\rail@begin{3}{classDecl}
    4.86 -\rail@nont{id}[]
    4.87 -\rail@bar
    4.88 -\rail@nextbar{1}
    4.89 -\rail@term{<}[]
    4.90 -\rail@plus
    4.91 -\rail@nont{id}[]
    4.92 -\rail@nextplus{2}
    4.93 -\rail@cterm{,}[]
    4.94 -\rail@endplus
    4.95 -\rail@endbar
    4.96 -\rail@end
    4.97 -\rail@begin{1}{default}
    4.98 -\rail@term{default}[]
    4.99 -\rail@nont{sort}[]
   4.100 -\rail@end
   4.101 -\rail@begin{4}{sort}
   4.102 -\rail@bar
   4.103 -\rail@nont{id}[]
   4.104 -\rail@nextbar{1}
   4.105 -\rail@token{lbrace}[]
   4.106 -\rail@bar
   4.107 -\rail@nextbar{2}
   4.108 -\rail@plus
   4.109 -\rail@nont{id}[]
   4.110 -\rail@nextplus{3}
   4.111 -\rail@cterm{,}[]
   4.112 -\rail@endplus
   4.113 -\rail@endbar
   4.114 -\rail@token{rbrace}[]
   4.115 -\rail@endbar
   4.116 -\rail@end
   4.117 -\rail@begin{3}{types}
   4.118 -\rail@term{types}[]
   4.119 -\rail@plus
   4.120 -\rail@nont{typeDecl}[]
   4.121 -\rail@bar
   4.122 -\rail@nextbar{1}
   4.123 -\rail@term{(}[]
   4.124 -\rail@nont{infix}[]
   4.125 -\rail@term{)}[]
   4.126 -\rail@endbar
   4.127 -\rail@nextplus{2}
   4.128 -\rail@endplus
   4.129 -\rail@end
   4.130 -\rail@begin{2}{infix}
   4.131 -\rail@bar
   4.132 -\rail@term{infixr}[]
   4.133 -\rail@nextbar{1}
   4.134 -\rail@term{infixl}[]
   4.135 -\rail@endbar
   4.136 -\rail@bar
   4.137 -\rail@nextbar{1}
   4.138 -\rail@nont{string}[]
   4.139 -\rail@endbar
   4.140 -\rail@nont{nat}[]
   4.141 -\rail@end
   4.142 -\rail@begin{3}{typeDecl}
   4.143 -\rail@nont{typevarlist}[]
   4.144 -\rail@nont{name}[]
   4.145 -\rail@bar
   4.146 -\rail@nextbar{1}
   4.147 -\rail@term{=}[]
   4.148 -\rail@bar
   4.149 -\rail@nont{string}[]
   4.150 -\rail@nextbar{2}
   4.151 -\rail@nont{type}[]
   4.152 -\rail@endbar
   4.153 -\rail@endbar
   4.154 -\rail@end
   4.155 -\rail@begin{4}{typevarlist}
   4.156 -\rail@bar
   4.157 -\rail@nextbar{1}
   4.158 -\rail@nont{tid}[]
   4.159 -\rail@nextbar{2}
   4.160 -\rail@term{(}[]
   4.161 -\rail@plus
   4.162 -\rail@nont{tid}[]
   4.163 -\rail@nextplus{3}
   4.164 -\rail@cterm{,}[]
   4.165 -\rail@endplus
   4.166 -\rail@term{)}[]
   4.167 -\rail@endbar
   4.168 -\rail@end
   4.169 -\rail@begin{5}{type}
   4.170 -\rail@bar
   4.171 -\rail@nont{simpleType}[]
   4.172 -\rail@nextbar{1}
   4.173 -\rail@term{(}[]
   4.174 -\rail@nont{type}[]
   4.175 -\rail@term{)}[]
   4.176 -\rail@nextbar{2}
   4.177 -\rail@nont{type}[]
   4.178 -\rail@term{=>}[]
   4.179 -\rail@nont{type}[]
   4.180 -\rail@nextbar{3}
   4.181 -\rail@term{[}[]
   4.182 -\rail@plus
   4.183 -\rail@nont{type}[]
   4.184 -\rail@nextplus{4}
   4.185 -\rail@cterm{,}[]
   4.186 -\rail@endplus
   4.187 -\rail@term{]}[]
   4.188 -\rail@term{=>}[]
   4.189 -\rail@nont{type}[]
   4.190 -\rail@endbar
   4.191 -\rail@end
   4.192 -\rail@begin{6}{simpleType}
   4.193 -\rail@bar
   4.194 -\rail@nont{id}[]
   4.195 -\rail@nextbar{1}
   4.196 -\rail@nont{tid}[]
   4.197 -\rail@bar
   4.198 -\rail@nextbar{2}
   4.199 -\rail@term{::}[]
   4.200 -\rail@nont{id}[]
   4.201 -\rail@endbar
   4.202 -\rail@nextbar{3}
   4.203 -\rail@term{(}[]
   4.204 -\rail@plus
   4.205 -\rail@nont{type}[]
   4.206 -\rail@nextplus{4}
   4.207 -\rail@cterm{,}[]
   4.208 -\rail@endplus
   4.209 -\rail@term{)}[]
   4.210 -\rail@nont{id}[]
   4.211 -\rail@nextbar{5}
   4.212 -\rail@nont{simpleType}[]
   4.213 -\rail@nont{id}[]
   4.214 -\rail@endbar
   4.215 -\rail@end
   4.216 -\rail@begin{3}{arities}
   4.217 -\rail@term{arities}[]
   4.218 -\rail@plus
   4.219 -\rail@plus
   4.220 -\rail@nont{name}[]
   4.221 -\rail@nextplus{1}
   4.222 -\rail@cterm{,}[]
   4.223 -\rail@endplus
   4.224 -\rail@term{::}[]
   4.225 -\rail@nont{arity}[]
   4.226 -\rail@nextplus{2}
   4.227 -\rail@endplus
   4.228 -\rail@end
   4.229 -\rail@begin{3}{arity}
   4.230 -\rail@bar
   4.231 -\rail@nextbar{1}
   4.232 -\rail@term{(}[]
   4.233 -\rail@plus
   4.234 -\rail@nont{sort}[]
   4.235 -\rail@nextplus{2}
   4.236 -\rail@cterm{,}[]
   4.237 -\rail@endplus
   4.238 -\rail@term{)}[]
   4.239 -\rail@endbar
   4.240 -\rail@nont{sort}[]
   4.241 -\rail@end
   4.242 -\rail@begin{2}{nonterminals}
   4.243 -\rail@term{nonterminals}[]
   4.244 -\rail@plus
   4.245 -\rail@nont{name}[]
   4.246 -\rail@nextplus{1}
   4.247 -\rail@endplus
   4.248 -\rail@end
   4.249 -\rail@begin{2}{consts}
   4.250 -\rail@term{consts}[]
   4.251 -\rail@plus
   4.252 -\rail@nont{mixfixConstDecl}[]
   4.253 -\rail@nextplus{1}
   4.254 -\rail@endplus
   4.255 -\rail@end
   4.256 -\rail@begin{2}{syntax}
   4.257 -\rail@term{syntax}[]
   4.258 -\rail@bar
   4.259 -\rail@nextbar{1}
   4.260 -\rail@nont{mode}[]
   4.261 -\rail@endbar
   4.262 -\rail@plus
   4.263 -\rail@nont{mixfixConstDecl}[]
   4.264 -\rail@nextplus{1}
   4.265 -\rail@endplus
   4.266 -\rail@end
   4.267 -\rail@begin{2}{mode}
   4.268 -\rail@term{(}[]
   4.269 -\rail@nont{name}[]
   4.270 -\rail@bar
   4.271 -\rail@nextbar{1}
   4.272 -\rail@term{output}[]
   4.273 -\rail@endbar
   4.274 -\rail@term{)}[]
   4.275 -\rail@end
   4.276 -\rail@begin{2}{mixfixConstDecl}
   4.277 -\rail@nont{constDecl}[]
   4.278 -\rail@bar
   4.279 -\rail@nextbar{1}
   4.280 -\rail@term{(}[]
   4.281 -\rail@nont{mixfix}[]
   4.282 -\rail@term{)}[]
   4.283 -\rail@endbar
   4.284 -\rail@end
   4.285 -\rail@begin{2}{constDecl}
   4.286 -\rail@plus
   4.287 -\rail@nont{name}[]
   4.288 -\rail@nextplus{1}
   4.289 -\rail@cterm{,}[]
   4.290 -\rail@endplus
   4.291 -\rail@term{::}[]
   4.292 -\rail@bar
   4.293 -\rail@nont{string}[]
   4.294 -\rail@nextbar{1}
   4.295 -\rail@nont{type}[]
   4.296 -\rail@endbar
   4.297 -\rail@end
   4.298 -\rail@begin{6}{mixfix}
   4.299 -\rail@bar
   4.300 -\rail@nont{string}[]
   4.301 -\rail@bar
   4.302 -\rail@nextbar{1}
   4.303 -\rail@bar
   4.304 -\rail@nextbar{2}
   4.305 -\rail@term{[}[]
   4.306 -\rail@plus
   4.307 -\rail@nont{nat}[]
   4.308 -\rail@nextplus{3}
   4.309 -\rail@cterm{,}[]
   4.310 -\rail@endplus
   4.311 -\rail@term{]}[]
   4.312 -\rail@endbar
   4.313 -\rail@nont{nat}[]
   4.314 -\rail@endbar
   4.315 -\rail@nextbar{4}
   4.316 -\rail@nont{infix}[]
   4.317 -\rail@nextbar{5}
   4.318 -\rail@term{binder}[]
   4.319 -\rail@nont{string}[]
   4.320 -\rail@nont{nat}[]
   4.321 -\rail@endbar
   4.322 -\rail@end
   4.323 -\rail@begin{4}{trans}
   4.324 -\rail@term{translations}[]
   4.325 -\rail@plus
   4.326 -\rail@nont{pat}[]
   4.327 -\rail@bar
   4.328 -\rail@term{==}[]
   4.329 -\rail@nextbar{1}
   4.330 -\rail@term{=>}[]
   4.331 -\rail@nextbar{2}
   4.332 -\rail@term{<=}[]
   4.333 -\rail@endbar
   4.334 -\rail@nont{pat}[]
   4.335 -\rail@nextplus{3}
   4.336 -\rail@endplus
   4.337 -\rail@end
   4.338 -\rail@begin{2}{pat}
   4.339 -\rail@bar
   4.340 -\rail@nextbar{1}
   4.341 -\rail@term{(}[]
   4.342 -\rail@nont{id}[]
   4.343 -\rail@term{)}[]
   4.344 -\rail@endbar
   4.345 -\rail@nont{string}[]
   4.346 -\rail@end
   4.347 -\rail@begin{2}{rules}
   4.348 -\rail@term{rules}[]
   4.349 -\rail@plus
   4.350 -\rail@nont{id}[]
   4.351 -\rail@nont{string}[]
   4.352 -\rail@nextplus{1}
   4.353 -\rail@endplus
   4.354 -\rail@end
   4.355 -\rail@begin{2}{defs}
   4.356 -\rail@term{defs}[]
   4.357 -\rail@plus
   4.358 -\rail@nont{id}[]
   4.359 -\rail@nont{string}[]
   4.360 -\rail@nextplus{1}
   4.361 -\rail@endplus
   4.362 -\rail@end
   4.363 -\rail@begin{3}{constdefs}
   4.364 -\rail@term{constdefs}[]
   4.365 -\rail@plus
   4.366 -\rail@nont{name}[]
   4.367 -\rail@term{::}[]
   4.368 -\rail@bar
   4.369 -\rail@nont{string}[]
   4.370 -\rail@nextbar{1}
   4.371 -\rail@nont{type}[]
   4.372 -\rail@endbar
   4.373 -\rail@bar
   4.374 -\rail@nextbar{1}
   4.375 -\rail@nont{mixfix}[]
   4.376 -\rail@endbar
   4.377 -\rail@nont{string}[]
   4.378 -\rail@nextplus{2}
   4.379 -\rail@endplus
   4.380 -\rail@end
   4.381 -\rail@begin{3}{axclass}
   4.382 -\rail@term{axclass}[]
   4.383 -\rail@nont{classDecl}[]
   4.384 -\rail@bar
   4.385 -\rail@nextbar{1}
   4.386 -\rail@plus
   4.387 -\rail@nont{id}[]
   4.388 -\rail@nont{string}[]
   4.389 -\rail@nextplus{2}
   4.390 -\rail@endplus
   4.391 -\rail@endbar
   4.392 -\rail@end
   4.393 -\rail@begin{2}{instance}
   4.394 -\rail@term{instance}[]
   4.395 -\rail@bar
   4.396 -\rail@nont{name}[]
   4.397 -\rail@term{<}[]
   4.398 -\rail@nont{name}[]
   4.399 -\rail@nextbar{1}
   4.400 -\rail@nont{name}[]
   4.401 -\rail@term{::}[]
   4.402 -\rail@nont{arity}[]
   4.403 -\rail@endbar
   4.404 -\rail@nont{witness}[]
   4.405 -\rail@end
   4.406 -\rail@begin{5}{witness}
   4.407 -\rail@bar
   4.408 -\rail@nextbar{1}
   4.409 -\rail@term{(}[]
   4.410 -\rail@plus
   4.411 -\rail@bar
   4.412 -\rail@nont{string}[]
   4.413 -\rail@nextbar{2}
   4.414 -\rail@nont{id}[]
   4.415 -\rail@nextbar{3}
   4.416 -\rail@nont{longident}[]
   4.417 -\rail@endbar
   4.418 -\rail@nextplus{4}
   4.419 -\rail@cterm{,}[]
   4.420 -\rail@endplus
   4.421 -\rail@term{)}[]
   4.422 -\rail@endbar
   4.423 -\rail@bar
   4.424 -\rail@nextbar{1}
   4.425 -\rail@nont{verbatim}[]
   4.426 -\rail@endbar
   4.427 -\rail@end
   4.428 -\rail@begin{1}{oracle}
   4.429 -\rail@term{oracle}[]
   4.430 -\rail@nont{name}[]
   4.431 -\rail@term{=}[]
   4.432 -\rail@nont{name}[]
   4.433 -\rail@end
   4.434 -\rail@begin{1}{local}
   4.435 -\rail@term{local}[]
   4.436 -\rail@end
   4.437 -\rail@begin{1}{global}
   4.438 -\rail@term{global}[]
   4.439 -\rail@end
   4.440 -\rail@begin{2}{setup}
   4.441 -\rail@term{setup}[]
   4.442 -\rail@bar
   4.443 -\rail@nont{id}[]
   4.444 -\rail@nextbar{1}
   4.445 -\rail@nont{longident}[]
   4.446 -\rail@endbar
   4.447 -\rail@end
   4.448 -\rail@begin{1}{ml}
   4.449 -\rail@term{ML}[]
   4.450 -\rail@nont{text}[]
   4.451 -\rail@end
   4.452 -}
     5.1 --- a/doc-src/System/Makefile	Wed May 05 18:26:10 1999 +0200
     5.2 +++ b/doc-src/System/Makefile	Wed May 05 18:35:41 1999 +0200
     5.3 @@ -1,30 +1,25 @@
     5.4 -#  $Id$
     5.5 -#########################################################################
     5.6 -#									#
     5.7 -#	Makefile for the report "The Isabelle System Manual"		#
     5.8 -#									#
     5.9 -#########################################################################
    5.10 +#
    5.11 +# $Id$
    5.12 +#
    5.13 +
    5.14 +## targets
    5.15 +
    5.16 +default: dvi
    5.17 +dist: dvi
    5.18  
    5.19  
    5.20 -FILES =  system.tex \
    5.21 -	 ../iman.sty ../extra.sty
    5.22 +## dependencies
    5.23 +
    5.24 +include ../Makefile.in
    5.25 +
    5.26 +NAME = system
    5.27 +FILES = system.tex ../iman.sty ../extra.sty
    5.28  
    5.29 -system.dvi.gz:   $(FILES)
    5.30 -	test -r isabelle.eps || ln -s ../gfx/isabelle.eps .
    5.31 -	-rm system.dvi*
    5.32 -	latex system
    5.33 -	latex system
    5.34 -	../sedindex system
    5.35 -	latex system
    5.36 -	gzip -f system.dvi
    5.37 +dvi: $(NAME).dvi
    5.38  
    5.39 -dist:   $(FILES)
    5.40 -	test -r isabelle.eps || ln -s ../gfx/isabelle.eps .
    5.41 -	-rm system.dvi*
    5.42 -	latex system
    5.43 -	latex system
    5.44 -	../sedindex system
    5.45 -	latex system
    5.46 -
    5.47 -clean:
    5.48 -	@rm *.aux *.log *.toc *.idx
    5.49 +$(NAME).dvi: $(FILES) isabelle.eps
    5.50 +	touch $(NAME).ind
    5.51 +	$(LATEX) $(NAME)
    5.52 +	$(LATEX) $(NAME)
    5.53 +	$(SEDINDEX) $(NAME)
    5.54 +	$(LATEX) $(NAME)
     6.1 --- a/doc-src/System/system.ind	Wed May 05 18:26:10 1999 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,85 +0,0 @@
     6.4 -\begin{theindex}
     6.5 -
     6.6 -  \item {\tt browser} tool, 19
     6.7 -
     6.8 -  \indexspace
     6.9 -
    6.10 -  \item {\tt doc} tool, 8
    6.11 -  \item {\tt DVI_VIEWER} setting, 4
    6.12 -
    6.13 -  \indexspace
    6.14 -
    6.15 -  \item {\tt expandshort} tool, 8
    6.16 -
    6.17 -  \indexspace
    6.18 -
    6.19 -  \item {\tt findlogics} tool, 9
    6.20 -
    6.21 -  \indexspace
    6.22 -
    6.23 -  \item {\tt getenv} tool, 9
    6.24 -
    6.25 -  \indexspace
    6.26 -
    6.27 -  \item HTML, 12
    6.28 -
    6.29 -  \indexspace
    6.30 -
    6.31 -  \item {\tt INSTALL}, 1
    6.32 -  \item {\tt install} tool, 10
    6.33 -  \item {\tt installfonts} tool, 14
    6.34 -  \item {\tt ISABELLE} setting, 3
    6.35 -  \item {\tt Isabelle}, 1, 7
    6.36 -  \item {\tt isabelle}, 1, 4
    6.37 -  \item {\tt ISABELLE_BROWSER_INFO} setting, 4, 17
    6.38 -  \item {\tt ISABELLE_DOCS} setting, 4
    6.39 -  \item {\tt ISABELLE_HOME} setting, 2, 3
    6.40 -  \item {\tt ISABELLE_HOME_USER} setting, 3
    6.41 -  \item {\tt ISABELLE_INSTALL_FONTS} setting, 4
    6.42 -  \item {\tt ISABELLE_INSTALLFONTS} setting, 14
    6.43 -  \item {\tt ISABELLE_INTERFACE} setting, 4, 7
    6.44 -  \item {\tt ISABELLE_LOGIC} setting, 4
    6.45 -  \item {\tt ISABELLE_OUTPUT} setting, 3, 4
    6.46 -  \item {\tt ISABELLE_PATH} setting, 3, 4
    6.47 -  \item {\tt ISABELLE_TMP_PREFIX} setting, 4
    6.48 -  \item {\tt ISABELLE_TOOLS} setting, 4
    6.49 -  \item {\tt ISABELLE_USEDIR_OPTIONS} setting, 4, 12, 17
    6.50 -  \item {\tt IsaMakefile}, 11, 12
    6.51 -  \item {\tt ISATOOL} setting, 3
    6.52 -  \item {\tt isatool}, 1, 7
    6.53 -
    6.54 -  \indexspace
    6.55 -
    6.56 -  \item {\tt logo} tool, 11
    6.57 -
    6.58 -  \indexspace
    6.59 -
    6.60 -  \item {\tt make} tool, 11
    6.61 -  \item {\tt makeall} tool, 12
    6.62 -  \item {\tt ML_HOME} setting, 3
    6.63 -  \item {\tt ML_IDENTIFIER} setting, 3
    6.64 -  \item {\tt ML_OPTIONS} setting, 3
    6.65 -  \item {\tt ML_PLATFORM} setting, 3
    6.66 -  \item {\tt ML_SYSTEM} setting, 3
    6.67 -
    6.68 -  \indexspace
    6.69 -
    6.70 -  \item {\tt nonascii} tool, 15
    6.71 -
    6.72 -  \indexspace
    6.73 -
    6.74 -  \item settings, \bold{1}
    6.75 -  \item {\tt symbolinput} tool, 16
    6.76 -  \item {\tt symbols}, 14
    6.77 -
    6.78 -  \indexspace
    6.79 -
    6.80 -  \item theory browsing information, \bold{17}
    6.81 -  \item theory graph browser, \bold{18}
    6.82 -
    6.83 -  \indexspace
    6.84 -
    6.85 -  \item {\tt use_dir}, 18
    6.86 -  \item {\tt usedir} tool, 12
    6.87 -
    6.88 -\end{theindex}
     7.1 --- a/doc-src/Tutorial/Makefile	Wed May 05 18:26:10 1999 +0200
     7.2 +++ b/doc-src/Tutorial/Makefile	Wed May 05 18:35:41 1999 +0200
     7.3 @@ -1,34 +1,29 @@
     7.4 -#  $Id$
     7.5 -#########################################################################
     7.6 -#									#
     7.7 -#	Makefile for the report "Isabelle/HOL. The Tutorial"		#
     7.8 -#									#
     7.9 -#########################################################################
    7.10 +#
    7.11 +# $Id$
    7.12 +#
    7.13 +
    7.14 +## targets
    7.15 +
    7.16 +default: dvi
    7.17 +dist: dvi
    7.18  
    7.19  
    7.20 -FILES =  tutorial.tex basics.tex fp.tex appendix.tex \
    7.21 -	 ../iman.sty ttbox.sty extra.sty
    7.22 +## dependencies
    7.23 +
    7.24 +include ../Makefile.in
    7.25 +
    7.26 +NAME = tutorial
    7.27 +FILES = tutorial.tex basics.tex fp.tex appendix.tex \
    7.28 +	../iman.sty ttbox.sty extra.sty
    7.29 +
    7.30 +dvi: $(NAME).dvi
    7.31  
    7.32 -tutorial.ps.gz:   $(FILES)
    7.33 -	isatool make
    7.34 -	test -r isabelle_hol.eps || ln -s ../gfx/isabelle_hol.eps .
    7.35 -	-rm tutorial.dvi*
    7.36 -	latex tutorial
    7.37 -	bibtex tutorial
    7.38 -	latex tutorial
    7.39 -	latex tutorial
    7.40 -	../sedindex tutorial
    7.41 -	latex tutorial
    7.42 -	dvips tutorial.dvi -o tutorial.ps
    7.43 -	gzip tutorial.ps
    7.44 -
    7.45 -dist:   $(FILES) 
    7.46 -	test -r isabelle_hol.eps || ln -s ../gfx/isabelle_hol.eps .
    7.47 -	-rm tutorial.dvi*
    7.48 -	latex tutorial
    7.49 -	latex tutorial
    7.50 -	../sedindex tutorial
    7.51 -	latex tutorial
    7.52 -
    7.53 -clean:
    7.54 -	@rm *.aux *.log *.toc *.idx
    7.55 +$(NAME).dvi: $(FILES) isabelle_hol.eps
    7.56 +	touch $(NAME).ind
    7.57 +	$(LATEX) $(NAME)
    7.58 +	$(RAIL) $(NAME)
    7.59 +	$(BIBTEX) $(NAME)
    7.60 +	$(LATEX) $(NAME)
    7.61 +	$(LATEX) $(NAME)
    7.62 +	$(SEDINDEX) $(NAME)
    7.63 +	$(LATEX) $(NAME)
     8.1 --- a/doc-src/Tutorial/tutorial.bbl	Wed May 05 18:26:10 1999 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,49 +0,0 @@
     8.4 -\begin{thebibliography}{1}
     8.5 -
     8.6 -\bibitem{Bird-Wadler}
     8.7 -Richard Bird and Philip Wadler.
     8.8 -\newblock {\em Introduction to Functional Programming}.
     8.9 -\newblock Prentice-Hall, 1988.
    8.10 -
    8.11 -\bibitem{Gunter-HOL92}
    8.12 -Elsa~L. Gunter.
    8.13 -\newblock Why we can't have {SML} style datatype declarations in {HOL}.
    8.14 -\newblock In L.J.M. Claesen and M.J.C. Gordon, editors, {\em Higher Order Logic
    8.15 -  Theorem Proving and its Applications: Proc.\ IFIP TC10/WG10.2 Intl. Workshop,
    8.16 -  1992}, pages 561--568. North-Holland, 1993.
    8.17 -
    8.18 -\bibitem{Knuth3-75}
    8.19 -Donald~E. Knuth.
    8.20 -\newblock {\em The Art of Computer Programming, Volume 3: Sorting and
    8.21 -  Searching}.
    8.22 -\newblock Addison-Wesley, 1975.
    8.23 -
    8.24 -\bibitem{MuellerNvOS98}
    8.25 -Olaf M\"uller, Tobias Nipkow, David~von Oheimb, and Oskar Slotosch.
    8.26 -\newblock {HOLCF = HOL + LCF}.
    8.27 -\newblock {\em J. Functional Programming}, 1999.
    8.28 -\newblock To appear.
    8.29 -
    8.30 -\bibitem{Isa-Ref-Man}
    8.31 -Lawrence~C. Paulson.
    8.32 -\newblock {\em The Isabelle Reference Manual}.
    8.33 -\newblock University of Cambridge, Computer Laboratory.
    8.34 -\newblock \verb$http://www.in.tum.de/~isabelle/dist/$.
    8.35 -
    8.36 -\bibitem{Isa-Logics-Man}
    8.37 -Lawrence~C. Paulson.
    8.38 -\newblock {\em Isabelle's Object-Logics}.
    8.39 -\newblock University of Cambridge, Computer Laboratory.
    8.40 -\newblock \verb$http://www.in.tum.de/~isabelle/dist/$.
    8.41 -
    8.42 -\bibitem{Paulson-LCF}
    8.43 -Lawrence~C. Paulson.
    8.44 -\newblock {\em Logic and Computation}.
    8.45 -\newblock Cambridge University Press, 1987.
    8.46 -
    8.47 -\bibitem{Paulson-ML}
    8.48 -Lawrence~C. Paulson.
    8.49 -\newblock {\em ML for the Working Programmer}.
    8.50 -\newblock Cambridge University Press, 2nd edition, 1996.
    8.51 -
    8.52 -\end{thebibliography}
     9.1 --- a/doc-src/Tutorial/tutorial.ind	Wed May 05 18:26:10 1999 +0200
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,148 +0,0 @@
     9.4 -\begin{theindex}
     9.5 -
     9.6 -  \item {\tt[]}, \bold{7}
     9.7 -  \item {\tt\#}, \bold{7}
     9.8 -  \item {\ttnot}, \bold{3}
     9.9 -  \item {\tt-->}, \bold{3}
    9.10 -  \item {\tt\&}, \bold{3}
    9.11 -  \item {\ttor}, \bold{3}
    9.12 -  \item {\tt?}, \bold{3}, 4
    9.13 -  \item {\ttall}, \bold{3}
    9.14 -  \item {\ttuniquex}, \bold{3}
    9.15 -  \item {\tt *}, \bold{17}
    9.16 -  \item {\tt +}, \bold{17}
    9.17 -  \item {\tt -}, \bold{17, 18}
    9.18 -  \item {\tt <}, \bold{17}
    9.19 -  \item {\tt <=}, \bold{17}
    9.20 -  \item \ttlbr, \bold{9}
    9.21 -  \item \ttrbr, \bold{9}
    9.22 -  \item {\tt==>}, \bold{9}
    9.23 -  \item {\tt==}, \bold{19}
    9.24 -  \item {\tt\%}, \bold{3}
    9.25 -  \item {\tt =>}, \bold{2}
    9.26 -
    9.27 -  \indexspace
    9.28 -
    9.29 -  \item {\tt addsimps}, \bold{22}
    9.30 -  \item {\tt Addsplits}, \bold{24}
    9.31 -  \item {\tt addsplits}, \bold{24}
    9.32 -  \item {\tt and}, \bold{29}
    9.33 -  \item {\tt arith_tac}, \bold{17}
    9.34 -  \item arithmetic, 17--18, 24
    9.35 -  \item {\tt Asm_full_simp_tac}, \bold{21}
    9.36 -  \item {\tt asm_full_simp_tac}, \bold{22}
    9.37 -  \item {\tt Asm_simp_tac}, \bold{21}
    9.38 -  \item {\tt asm_simp_tac}, \bold{22}
    9.39 -
    9.40 -  \indexspace
    9.41 -
    9.42 -  \item {\tt bool}, 2
    9.43 -
    9.44 -  \indexspace
    9.45 -
    9.46 -  \item {\tt case}, \bold{3}, 4, \bold{13}, 24
    9.47 -  \item {\tt constdefs}, \bold{19}
    9.48 -  \item {\tt consts}, \bold{7}
    9.49 -  \item {\tt context}, \bold{11}
    9.50 -  \item current theory, \bold{11}
    9.51 -
    9.52 -  \indexspace
    9.53 -
    9.54 -  \item {\tt datatype}, \bold{7}, 29--33
    9.55 -  \item {\tt defs}, \bold{19}
    9.56 -  \item {\tt delsimps}, \bold{22}
    9.57 -  \item {\tt Delsplits}, \bold{24}
    9.58 -  \item {\tt delsplits}, \bold{24}
    9.59 -  \item {\tt div}, \bold{17}
    9.60 -
    9.61 -  \indexspace
    9.62 -
    9.63 -  \item {\tt exhaust_tac}, \bold{14}
    9.64 -
    9.65 -  \indexspace
    9.66 -
    9.67 -  \item {\tt False}, \bold{3}
    9.68 -  \item formula, \bold{3}
    9.69 -  \item {\tt Full_simp_tac}, \bold{21}
    9.70 -  \item {\tt full_simp_tac}, \bold{22}
    9.71 -
    9.72 -  \indexspace
    9.73 -
    9.74 -  \item {\tt hd}, \bold{12}
    9.75 -
    9.76 -  \indexspace
    9.77 -
    9.78 -  \item {\tt if}, \bold{3}, 4, 24
    9.79 -  \item {\tt infixr}, \bold{7}
    9.80 -  \item inner syntax, \bold{8}
    9.81 -
    9.82 -  \indexspace
    9.83 -
    9.84 -  \item {\tt LEAST}, \bold{17}
    9.85 -  \item {\tt let}, \bold{3}, 4, 23
    9.86 -  \item {\tt list}, 2
    9.87 -  \item loading theories, 12
    9.88 -
    9.89 -  \indexspace
    9.90 -
    9.91 -  \item {\tt Main}, \bold{2}
    9.92 -  \item {\tt max}, \bold{17, 18}
    9.93 -  \item measure function, \bold{36}
    9.94 -  \item {\tt min}, \bold{17, 18}
    9.95 -  \item {\tt mod}, \bold{17}
    9.96 -  \item {\tt mutual_induct_tac}, \bold{30}
    9.97 -
    9.98 -  \indexspace
    9.99 -
   9.100 -  \item {\tt nat}, 2, \bold{17}
   9.101 -  \item {\tt None}, \bold{33}
   9.102 -
   9.103 -  \indexspace
   9.104 -
   9.105 -  \item {\tt option}, \bold{33}
   9.106 -
   9.107 -  \indexspace
   9.108 -
   9.109 -  \item parent theory, \bold{1}
   9.110 -  \item primitive recursion, \bold{13}
   9.111 -  \item {\tt primrec}, 7, \bold{13}, 29--33
   9.112 -  \item proof scripts, \bold{2}
   9.113 -
   9.114 -  \indexspace
   9.115 -
   9.116 -  \item {\tt recdef}, 35--38
   9.117 -  \item reloading theories, 12
   9.118 -
   9.119 -  \indexspace
   9.120 -
   9.121 -  \item schematic variable, \bold{4}
   9.122 -  \item {\tt set}, 2
   9.123 -  \item {\tt show_brackets}, \bold{4}
   9.124 -  \item {\tt show_types}, \bold{3}, 11
   9.125 -  \item {\tt Simp_tac}, \bold{21}
   9.126 -  \item {\tt simp_tac}, \bold{22}
   9.127 -  \item simplifier, \bold{20}
   9.128 -  \item simpset, \bold{21}
   9.129 -  \item {\tt Some}, \bold{33}
   9.130 -
   9.131 -  \indexspace
   9.132 -
   9.133 -  \item tactic, \bold{11}
   9.134 -  \item term, \bold{3}
   9.135 -  \item theory, \bold{1}
   9.136 -  \item {\tt tl}, \bold{12}
   9.137 -  \item total, \bold{7}
   9.138 -  \item tracing the simplifier, \bold{25}
   9.139 -  \item {\tt True}, \bold{3}
   9.140 -  \item type constraints, \bold{3}
   9.141 -  \item type inference, \bold{3}
   9.142 -  \item type synonyms, \bold{18}
   9.143 -  \item {\tt types}, \bold{18}
   9.144 -
   9.145 -  \indexspace
   9.146 -
   9.147 -  \item unknown, \bold{4}
   9.148 -  \item {\tt update_thy}, \bold{12}
   9.149 -  \item {\tt use_thy}, \bold{2}, 12
   9.150 -
   9.151 -\end{theindex}