Re: [isabelle] Typo in Tutorial?

Is there another tutorial resource that you'd recommend over it?

I've been working through that tutorial, and was previously unaware it was outdated.

Daniel Horne

----- Original Message ----- From: "Tobias Nipkow" <nipkow at>
To: <cl-isabelle-users at>
Sent: Wednesday, February 25, 2015 12:10 PM
Subject: Re: [isabelle] Typo in Tutorial?

Yes inded, this is the result of a change. In the past we had plus_ac and
times_ac, now we have ac_simps (although the others still exist). The tutorial, although technically still correct, is not state of the art any longer. Hence we don't invest much energy when updating it. But thanks for pointing this out, it
would be better to fix it.


On 25/02/2015 03:43, Andrew Gacek wrote:
In the Isabelle/HOL tutorial [1] at the top of page 172 the text
refers to "ac_simps" and "ac_simps" as if they mean two different
things. Is this a typo or am I missing something else? For example:

"The name ac_simps refers to the list of all three theorems; similarly
there is ac_simps."

"Simplify using ac_simps and ac_simps."

"apply (simp add: ac_simps ac_simps)"

It looks like some kind of search/replace went wrong perhaps?



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.