ch7_tactics_automation/index.html

<html>
<title> Tactics and automation </title>
<body bgcolor=#08FFFF>
<h1>  Tactics and automation  </h1>

<a href="SRC/chap7.v"> The complete sources of this chapter </a>

<h2> Exercises </h2>
<ul>

<li> <a href= "primes_hyps.html"> Exercise 7.1 page 204 </a> Some lemmas about divisibility 
<li> <a href= "Zpos_x_tac.html"> Exercise 7.2 page 209 </a> Rewriting with exceptions
<li> <a href= "le_lt_S_eq.html"> using omega </a> Using omega

</ul>
<h2> Errata </h2>
<ol>
<li> Page 195, section 7.3.2:<br>
read: 
<quote>
"The <tt>subst</tt> tactic looks for hypotheses of the form 
<em>x = exp </em> or <em> exp = x </em>"
</quote>

<li> Page 196, end of the first paragraph: 
read: <quote>
"It is however, a good complement to our <tt>caseEq</tt> tactic ..."
</quote>

<li> Section  7.1.2.2, paragraph 2, page 189: <br>
     
read "Moreover, the argument delta" instead of "Moreover, the argument Delta"

<li>
 Page 209. "[|- context [(S ?1)]]" should be replaced by "[|- context [(S ?X1)]]"

<li>
 Page 209 (fifth paragraph) replace "match ?1" by "match X1"
<li> Page 210 (last paragraph) read "simpl_on" instead of "simpl_On" 

<li> Section  7.6.2.1, page 203: <br>
     
read "The patterns have the form <br>
 <tt> [h1:t1, h2:t2, ... |- C]</tt>"

<br> (instead of  <tt> [h1:t1; h2:t2, ... |- C]</tt>


</ol>

<hr>


</body>
</html>