doc-src/Ref/ref.ind
changeset 3524 c02cb15830de
parent 3498 807549666b9c
child 3562 5380acac8c83
equal deleted inserted replaced
3523:23eae933c2d9 3524:c02cb15830de
   244     \subitem of simplification, 106
   244     \subitem of simplification, 106
   245     \subitem of translations, 92
   245     \subitem of translations, 92
   246   \item exceptions
   246   \item exceptions
   247     \subitem printing of, 5
   247     \subitem printing of, 5
   248   \item {\tt exit}, \bold{2}
   248   \item {\tt exit}, \bold{2}
   249   \item {\tt extensional}, \bold{44}
   249   \item {\tt extensional}, \bold{43}
   250 
   250 
   251   \indexspace
   251   \indexspace
   252 
   252 
   253   \item {\tt fa}, \bold{11}
   253   \item {\tt fa}, \bold{11}
   254   \item {\tt Fast_tac}, \bold{128}
   254   \item {\tt Fast_tac}, \bold{128}
   276   \item {\tt fold_goals_tac}, \bold{20}
   276   \item {\tt fold_goals_tac}, \bold{20}
   277   \item {\tt fold_tac}, \bold{20}
   277   \item {\tt fold_tac}, \bold{20}
   278   \item {\tt forall_elim}, \bold{44}
   278   \item {\tt forall_elim}, \bold{44}
   279   \item {\tt forall_elim_list}, \bold{44}
   279   \item {\tt forall_elim_list}, \bold{44}
   280   \item {\tt forall_elim_var}, \bold{44}
   280   \item {\tt forall_elim_var}, \bold{44}
   281   \item {\tt forall_elim_vars}, \bold{45}
   281   \item {\tt forall_elim_vars}, \bold{44}
   282   \item {\tt forall_intr}, \bold{44}
   282   \item {\tt forall_intr}, \bold{44}
   283   \item {\tt forall_intr_frees}, \bold{44}
   283   \item {\tt forall_intr_frees}, \bold{44}
   284   \item {\tt forall_intr_list}, \bold{44}
   284   \item {\tt forall_intr_list}, \bold{44}
   285   \item {\tt force_strip_shyps}, \bold{40}
   285   \item {\tt force_strip_shyps}, \bold{40}
   286   \item {\tt forw_inst_tac}, \bold{18}
   286   \item {\tt forw_inst_tac}, \bold{18}
   323   \item {\tt iff_reflection} theorem, 113
   323   \item {\tt iff_reflection} theorem, 113
   324   \item {\tt imp_intr} theorem, \bold{97}
   324   \item {\tt imp_intr} theorem, \bold{97}
   325   \item {\tt implies_elim}, \bold{43}
   325   \item {\tt implies_elim}, \bold{43}
   326   \item {\tt implies_elim_list}, \bold{43}
   326   \item {\tt implies_elim_list}, \bold{43}
   327   \item {\tt implies_intr}, \bold{42}
   327   \item {\tt implies_intr}, \bold{42}
   328   \item {\tt implies_intr_hyps}, \bold{43}
   328   \item {\tt implies_intr_hyps}, \bold{42}
   329   \item {\tt implies_intr_list}, \bold{42}
   329   \item {\tt implies_intr_list}, \bold{42}
   330   \item {\tt incr_boundvars}, \bold{58}, 92
   330   \item {\tt incr_boundvars}, \bold{58}, 92
   331   \item {\tt indexname} ML type, 57, 67
   331   \item {\tt indexname} ML type, 57, 67
   332   \item infixes, \bold{73}
   332   \item infixes, \bold{73}
   333   \item {\tt insert} constant, 88
   333   \item {\tt insert} constant, 88