Error in the tutorial at 3.3.2.1

[Hibou57]

At 3.3.2.1, the tutorial says to try this:

- g ‘!m. m + 0 = m‘;
- e (INDUCT_TAC THENL [REWRITE_TAC[ADD], ASM_REWRITE_TAC[ADD]]);

An open (I don't know what to open) seems to be missing, as I get this error:

Error-Value or constructor (INDUCT_TAC) has not been declared
Found near e (INDUCT_TAC THENL [REWRITE_TAC [ADD], ASM_REWRITE_TAC [...]])
Error-Value or constructor (ADD) has not been declared Found near [ADD]
Error-Value or constructor (ADD) has not been declared Found near [ADD]
Static Errors

The box is numbered 1, so this is the start of an example session.

[Hibou57]

By the way, 3.3.2.2 says “The tactical THEN is an ML infix”: The section 3.3.2.1 could say the same about THENL (as it comes before).

[Hibou57]

I don't know if I should open a new issue or not. I have found another error, or rather, unexpected result.

On page 50, the tutorial suggest to try to solve a subgoal in a way which is supposed to fail, however, it actually succeed. Oops, unexpected success …

The tutorial says:

- e (RW_TAC arith_ss []);
OK..
1 subgoal:
> val it =
    SUC n <= x * SUC n \/ (x = 0)

Doing so, I get this instead:

> e (RW_TAC arith_ss []);
OK..

Goal proved.
|- SUC n ≤ SUC n * x ∨ (SUC n * x = 0)

Goal proved.
|- m ≤ m * x ∨ (m * x = 0)
val it =
   Initial goal proved.
|- ∀m n. m divides n ⇒ m ≤ n ∨ (n = 0):
   proof

[mn200]

Thanks for the reports. The tutorial's third chapter is going to be rewritten fairly significantly before our next release (see issue #275). I'll fix the description of what happens in the Euclid proof today.

[Hibou57]

Thanks :-)

[mn200]

As of bf01cd8, the Logic chapter has been entirely removed. If reinstated, it will appear later in the Tutorial. Given that much of this stuff is already covered fairly well in the Description, I don't think its absence will be a major problem.