1120   the rules, use the tactic combinator @{ML_ind  DEPTH_SOLVE}, which searches 

  1120   the rules, use the tactic combinator @{ML_ind  DEPTH_SOLVE}, which searches 

  1121   for a state in which all subgoals are solved. Add also rules for equality and

  1121   for a state in which all subgoals are solved. Add also rules for equality and

  1122   run your tactic on the de Bruijn formulae discussed in Exercise~\ref{ex:debruijn}. 

  1122   run your tactic on the de Bruijn formulae discussed in Exercise~\ref{ex:debruijn}. 

  1123   \end{exercise}

  1123   \end{exercise}

  1124 

  1124 

  1125 *}

  1127 *}

  1126 

  1128 

  1127 section {* Simplifier Tactics *}

  1129 section {* Simplifier Tactics *}

  1128 

  1130 

  1129 text {*

  1131 text {*