fix(04,08,11,13): fix chapters to reflect changes in Lean. Closes #196.

[avigad]

This fix adapts to recent changes in Lean, notably the removal of by+, assert, etc.

The tutorial needs an overhaul, and I have a list of corrections Nathan Carter that is now almost a year old. But at this point it seems to make sense to wait for Lean 3, and revise the tutorial for the new system.

@leodemoura I am not sure what to say about the semicolon in tactic mode. You removed backtracking, right? So is there any difference between by foo; bar and begin foo, bar end?

[soonhokong]

@avigad, Making_Auxiliary_Facts_Visible is commented out here, but still used in Chapter 12. Could you take care of it?

[avigad]

@soonhokong My bad. I just added that fix. Now "make test" and "make" both succeed, so hopefully we're good.

[soonhokong]

@avigad, thanks! I'll close this issue and process other PRs tonight.

[leodemoura]

@leodemoura I am not sure what to say about the semicolon in tactic mode. You removed backtracking, right? So is there any difference between by foo; bar and begin foo, bar end?

The master branch still implements backtracking. So, this part is fine for now.
After the refactoring, and lean3 becomes the main branch, we will need a major change in the tactic section.
We will use the monadic do notation (like Haskell) for writing tactic scripts.
I'm planning to keep the begin - end blocks for "interactive use". The main difference will be implicit quotation, and ,-notation for entering a sequence of tactics.

[avigad]

I'm looking forward to the new tactic language.

Something caused at least one of these two examples in the tutorial to break (I think it was the second one): 0fdeb02#diff-77be5851357653823680ddcaf7d93760R258

So I commented out the section. I think we can do without it.