auto generated
authorpaulson
Tue Mar 03 15:09:04 1998 +0100 (1998-03-03)
changeset 4671c45cdc1b5e09
parent 4670 f309259fa828
child 4672 9d55bc687e1e
auto generated
doc-src/Ref/ref.ind
     1.1 --- a/doc-src/Ref/ref.ind	Sat Feb 28 15:41:50 1998 +0100
     1.2 +++ b/doc-src/Ref/ref.ind	Tue Mar 03 15:09:04 1998 +0100
     1.3 @@ -26,29 +26,29 @@
     1.4    \item {\tt abstract_over}, \bold{61}
     1.5    \item {\tt abstract_rule}, \bold{45}
     1.6    \item {\tt aconv}, \bold{61}
     1.7 -  \item {\tt addaltern}, \bold{133}
     1.8 -  \item {\tt addbefore}, \bold{133}
     1.9 +  \item {\tt addaltern}, \bold{134}
    1.10 +  \item {\tt addbefore}, \bold{134}
    1.11    \item {\tt Addcongs}, \bold{105}
    1.12    \item {\tt addcongs}, \bold{109}, 124, 125
    1.13 -  \item {\tt AddDs}, \bold{137}
    1.14 +  \item {\tt AddDs}, \bold{138}
    1.15    \item {\tt addDs}, \bold{132}
    1.16    \item {\tt addeqcongs}, \bold{109}, 124
    1.17 -  \item {\tt AddEs}, \bold{137}
    1.18 +  \item {\tt AddEs}, \bold{138}
    1.19    \item {\tt addEs}, \bold{132}
    1.20 -  \item {\tt AddIs}, \bold{137}
    1.21 +  \item {\tt AddIs}, \bold{138}
    1.22    \item {\tt addIs}, \bold{132}
    1.23    \item {\tt addloop}, \bold{112}
    1.24    \item {\tt addSaltern}, \bold{133}
    1.25    \item {\tt addSbefore}, \bold{133}
    1.26 -  \item {\tt AddSDs}, \bold{137}
    1.27 +  \item {\tt AddSDs}, \bold{138}
    1.28    \item {\tt addSDs}, \bold{132}
    1.29 -  \item {\tt AddSEs}, \bold{137}
    1.30 +  \item {\tt AddSEs}, \bold{138}
    1.31    \item {\tt addSEs}, \bold{132}
    1.32    \item {\tt Addsimprocs}, \bold{105}
    1.33    \item {\tt addsimprocs}, \bold{108}
    1.34    \item {\tt Addsimps}, \bold{105}
    1.35 -  \item {\tt addsimps}, \bold{107}, 125
    1.36 -  \item {\tt AddSIs}, \bold{137}
    1.37 +  \item {\tt addsimps}, \bold{108}, 125
    1.38 +  \item {\tt AddSIs}, \bold{138}
    1.39    \item {\tt addSIs}, \bold{132}
    1.40    \item {\tt addSolver}, \bold{111}
    1.41    \item {\tt addsplits}, \bold{112}, 124, 126
    1.42 @@ -96,7 +96,7 @@
    1.43      \subitem made from parse trees, 84
    1.44      \subitem made from terms, 86
    1.45    \item {\tt atac}, \bold{20}
    1.46 -  \item {\tt Auto_tac}, \bold{137}
    1.47 +  \item {\tt Auto_tac}, \bold{138}
    1.48    \item {\tt axclass} section, 53
    1.49    \item axiomatic type class, 53
    1.50    \item axioms
    1.51 @@ -113,7 +113,7 @@
    1.52    \item {\tt be}, \bold{12}
    1.53    \item {\tt bes}, \bold{12}
    1.54    \item {\tt BEST_FIRST}, \bold{32}, 33
    1.55 -  \item {\tt Best_tac}, \bold{137}
    1.56 +  \item {\tt Best_tac}, \bold{138}
    1.57    \item {\tt best_tac}, \bold{136}
    1.58    \item {\tt beta_conversion}, \bold{45}
    1.59    \item {\tt bicompose}, \bold{48}
    1.60 @@ -121,10 +121,10 @@
    1.61    \item {\tt bind_thm}, \bold{9}, 10, 38
    1.62    \item binders, \bold{78}
    1.63    \item {\tt biresolution}, \bold{47}
    1.64 -  \item {\tt biresolve_tac}, \bold{24}, 138
    1.65 +  \item {\tt biresolve_tac}, \bold{24}, 139
    1.66    \item {\tt Blast.depth_tac}, \bold{135}
    1.67    \item {\tt Blast.trace}, \bold{135}
    1.68 -  \item {\tt Blast_tac}, \bold{137}
    1.69 +  \item {\tt Blast_tac}, \bold{138}
    1.70    \item {\tt blast_tac}, \bold{135}
    1.71    \item {\tt Bound}, \bold{60}, 84, 86, 87
    1.72    \item {\tt bound_hyp_subst_tac}, \bold{100}
    1.73 @@ -143,17 +143,17 @@
    1.74    \item {\tt CHANGED}, \bold{31}
    1.75    \item {\tt chop}, \bold{10}, 14
    1.76    \item {\tt choplev}, \bold{10}
    1.77 -  \item {\tt Clarify_step_tac}, \bold{137}
    1.78 +  \item {\tt Clarify_step_tac}, \bold{138}
    1.79    \item {\tt clarify_step_tac}, \bold{134}
    1.80 -  \item {\tt Clarify_tac}, \bold{137}
    1.81 +  \item {\tt Clarify_tac}, \bold{138}
    1.82    \item {\tt clarify_tac}, \bold{134}
    1.83    \item claset
    1.84      \subitem current, 137
    1.85    \item {\tt claset} ML type, 131
    1.86    \item classes
    1.87      \subitem context conditions, 54
    1.88 -  \item classical reasoner, 127--139
    1.89 -    \subitem setting up, 138
    1.90 +  \item classical reasoner, 127--140
    1.91 +    \subitem setting up, 139
    1.92      \subitem tactics, 134
    1.93    \item classical sets, 131
    1.94    \item {\tt ClassicalFun}, 139
    1.95 @@ -163,7 +163,7 @@
    1.96    \item {\tt compose}, \bold{47}
    1.97    \item {\tt compose_tac}, \bold{24}
    1.98    \item {\tt compSWrapper}, \bold{133}
    1.99 -  \item {\tt compWrapper}, \bold{133}
   1.100 +  \item {\tt compWrapper}, \bold{134}
   1.101    \item {\tt concl_of}, \bold{41}
   1.102    \item {\tt COND}, \bold{33}
   1.103    \item congruence rules, 109
   1.104 @@ -192,7 +192,7 @@
   1.105    \indexspace
   1.106  
   1.107    \item {\tt datatype}, 105
   1.108 -  \item {\tt Deepen_tac}, \bold{137}
   1.109 +  \item {\tt Deepen_tac}, \bold{138}
   1.110    \item {\tt deepen_tac}, \bold{136}
   1.111    \item {\tt defer_tac}, \bold{21}
   1.112    \item definitions, \see{rewriting, meta-level}{1}, 21, \bold{54}
   1.113 @@ -206,7 +206,7 @@
   1.114    \item {\tt Delsimprocs}, \bold{105}
   1.115    \item {\tt delsimprocs}, \bold{108}
   1.116    \item {\tt Delsimps}, \bold{105}
   1.117 -  \item {\tt delsimps}, \bold{107}
   1.118 +  \item {\tt delsimps}, \bold{108}
   1.119    \item {\tt dependent_tr'}, 94, \bold{96}
   1.120    \item {\tt DEPTH_FIRST}, \bold{32}
   1.121    \item {\tt DEPTH_SOLVE}, \bold{32}
   1.122 @@ -238,7 +238,7 @@
   1.123    \item elim-resolution, 17
   1.124    \item {\tt ematch_tac}, \bold{18}
   1.125    \item {\tt empty} constant, 92
   1.126 -  \item {\tt empty_cs}, \bold{131}
   1.127 +  \item {\tt empty_cs}, \bold{132}
   1.128    \item {\tt empty_ss}, \bold{106}
   1.129    \item {\tt eq_assume_tac}, \bold{18}, 131
   1.130    \item {\tt eq_assumption}, \bold{47}
   1.131 @@ -264,7 +264,7 @@
   1.132      \subitem of logic definitions, 80
   1.133      \subitem of macros, 92, 93
   1.134      \subitem of mixfix declarations, 75
   1.135 -    \subitem of simplification, 113
   1.136 +    \subitem of simplification, 114
   1.137      \subitem of translations, 96
   1.138    \item exceptions
   1.139      \subitem printing of, 5
   1.140 @@ -274,7 +274,7 @@
   1.141    \indexspace
   1.142  
   1.143    \item {\tt fa}, \bold{12}
   1.144 -  \item {\tt Fast_tac}, \bold{137}
   1.145 +  \item {\tt Fast_tac}, \bold{138}
   1.146    \item {\tt fast_tac}, \bold{136}
   1.147    \item {\tt fd}, \bold{12}
   1.148    \item {\tt fds}, \bold{12}
   1.149 @@ -339,8 +339,8 @@
   1.150    \item higher-order pattern, \bold{108}
   1.151    \item {\tt HOL_basic_ss}, \bold{106}
   1.152    \item {\tt hyp_subst_tac}, \bold{100}
   1.153 -  \item {\tt hyp_subst_tacs}, \bold{139}
   1.154 -  \item {\tt HypsubstFun}, 101, 139
   1.155 +  \item {\tt hyp_subst_tacs}, \bold{140}
   1.156 +  \item {\tt HypsubstFun}, 101, 140
   1.157  
   1.158    \indexspace
   1.159  
   1.160 @@ -373,7 +373,7 @@
   1.161  
   1.162    \indexspace
   1.163  
   1.164 -  \item {\tt joinrules}, \bold{138}
   1.165 +  \item {\tt joinrules}, \bold{139}
   1.166  
   1.167    \indexspace
   1.168  
   1.169 @@ -402,7 +402,7 @@
   1.170    \item {\tt Match} exception, 95
   1.171    \item {\tt match_tac}, \bold{18}, 131
   1.172    \item {\tt max_pri}, 68, \bold{74}
   1.173 -  \item {\tt merge_ss}, \bold{106}
   1.174 +  \item {\tt merge_ss}, \bold{107}
   1.175    \item {\tt merge_theories}, \bold{58}
   1.176    \item meta-assumptions, 34, 42, 44, 47
   1.177      \subitem printing of, 4
   1.178 @@ -410,7 +410,7 @@
   1.179    \item meta-implication, 43, 44
   1.180    \item meta-quantifiers, 43, 45
   1.181    \item meta-rewriting, 8, 13, 14, \bold{21}, 
   1.182 -		\seealso{tactics, theorems}{140}
   1.183 +		\seealso{tactics, theorems}{141}
   1.184      \subitem in theorems, 39
   1.185    \item meta-rules, \see{meta-rules}{1}, 42--48
   1.186    \item {\tt METAHYPS}, 16, \bold{34}
   1.187 @@ -472,7 +472,7 @@
   1.188    \item {\tt prin}, 6, \bold{15}
   1.189    \item print mode, 52, 97
   1.190    \item print modes, 78--79
   1.191 -  \item {\tt print_cs}, \bold{131}
   1.192 +  \item {\tt print_cs}, \bold{132}
   1.193    \item {\tt print_data}, \bold{59}
   1.194    \item {\tt print_depth}, \bold{4}
   1.195    \item {\tt print_exn}, \bold{6}, 37
   1.196 @@ -547,8 +547,10 @@
   1.197    \item {\tt rename_last_tac}, \bold{22}
   1.198    \item {\tt rename_params_rule}, \bold{48}
   1.199    \item {\tt rename_tac}, \bold{22}
   1.200 +  \item {\tt rep_cs}, \bold{132}
   1.201    \item {\tt rep_cterm}, \bold{62}
   1.202    \item {\tt rep_ctyp}, \bold{64}
   1.203 +  \item {\tt rep_ss}, \bold{106}
   1.204    \item {\tt rep_thm}, \bold{41}
   1.205    \item {\tt REPEAT}, \bold{30, 31}
   1.206    \item {\tt REPEAT1}, \bold{30}
   1.207 @@ -590,11 +592,11 @@
   1.208  
   1.209    \indexspace
   1.210  
   1.211 -  \item {\tt safe_asm_full_simp_tac}, \bold{112}
   1.212 -  \item {\tt Safe_step_tac}, \bold{137}
   1.213 -  \item {\tt safe_step_tac}, 132, \bold{136}
   1.214 -  \item {\tt Safe_tac}, \bold{137}
   1.215 -  \item {\tt safe_tac}, \bold{136}
   1.216 +  \item {\tt safe_asm_full_simp_tac}, \bold{113}
   1.217 +  \item {\tt Safe_step_tac}, \bold{138}
   1.218 +  \item {\tt safe_step_tac}, 133, \bold{137}
   1.219 +  \item {\tt Safe_tac}, \bold{138}
   1.220 +  \item {\tt safe_tac}, \bold{137}
   1.221    \item {\tt save_proof}, \bold{15}
   1.222    \item saving your work, \bold{1}
   1.223    \item search, 29
   1.224 @@ -612,7 +614,7 @@
   1.225    \item {\tt setsubgoaler}, \bold{110}, 125
   1.226    \item {\tt setSWrapper}, \bold{133}
   1.227    \item {\tt settermless}, \bold{117}
   1.228 -  \item {\tt setWrapper}, \bold{133}
   1.229 +  \item {\tt setWrapper}, \bold{134}
   1.230    \item shortcuts
   1.231      \subitem for tactics, 20
   1.232      \subitem for {\tt by} commands, 11
   1.233 @@ -639,11 +641,11 @@
   1.234      \subitem tactics, 112
   1.235    \item simplification sets, 106
   1.236    \item {\tt simplify}, 113
   1.237 -  \item {\tt SIMPSET}, \bold{112}
   1.238 +  \item {\tt SIMPSET}, \bold{113}
   1.239    \item simpset
   1.240      \subitem current, 103, 107
   1.241    \item {\tt simpset}, \bold{107}
   1.242 -  \item {\tt SIMPSET'}, \bold{112}
   1.243 +  \item {\tt SIMPSET'}, \bold{113}
   1.244    \item {\tt simpset_of}, \bold{107}
   1.245    \item {\tt simpset_ref}, \bold{107}
   1.246    \item {\tt simpset_ref_of}, \bold{107}
   1.247 @@ -666,7 +668,7 @@
   1.248    \item stamps, \bold{51}, 59
   1.249    \item {\tt standard}, \bold{40}
   1.250    \item starting up, \bold{1}
   1.251 -  \item {\tt Step_tac}, \bold{137}
   1.252 +  \item {\tt Step_tac}, \bold{138}
   1.253    \item {\tt step_tac}, 133, \bold{137}
   1.254    \item {\tt store_thm}, \bold{9}
   1.255    \item {\tt string_of_cterm}, \bold{62}
   1.256 @@ -684,7 +686,7 @@
   1.257    \item {\tt subthy}, \bold{58}
   1.258    \item {\tt swap} theorem, \bold{139}
   1.259    \item {\tt swap_res_tac}, \bold{138}
   1.260 -  \item {\tt swapify}, \bold{138}
   1.261 +  \item {\tt swapify}, \bold{139}
   1.262    \item {\tt sym} theorem, 100, \bold{102}
   1.263    \item {\tt symmetric}, \bold{45}
   1.264    \item {\tt syn_of}, \bold{72}