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
----- Original Message -----
From: "Tobias Nipkow" <nipkow at in.tum.de>
To: <cl-isabelle-users at lists.cam.ac.uk>
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
although technically still correct, is not state of the art any longer.
don't invest much energy when updating it. But thanks for pointing this out,
would be better to fix it.
On 25/02/2015 03:43, Andrew Gacek wrote:
In the Isabelle/HOL tutorial  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