Re: [isabelle] Typo in Tutorial?

The first of the tutorials (on the Isabelle pages), "Programming and Proving in Isabelle/HOL", covers structured proofs and deemphasizes "apply". It is meant as a compact intro and does not cover everything covered in the old tutorial.


On 26/02/2015 05:05, Daniel Horne wrote:
Is there another tutorial resource that you'd recommend over it?

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

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?



Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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