*To*: Daniel Horne <d.horne at danielhorne.co.uk>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Typo in Tutorial?*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 26 Feb 2015 07:42:48 +0100*In-reply-to*: <EDAF247BF47D480493AEC344DFB7DE6E@DuSTmanPC>*References*: <CAHgzvFjLRE0gYG-rvAYPcnnyEw1gZxuSnUGzStrVLvyQ1X+KbQ@mail.gmail.com> <54EDBBBF.4040409@in.tum.de> <EDAF247BF47D480493AEC344DFB7DE6E@DuSTmanPC>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:31.0) Gecko/20100101 Thunderbird/31.5.0

Tobias 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 outdated. Thanks Daniel Horne ----- 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 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. Tobias 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? -Andrew [1] http://isabelle.in.tum.de/doc/tutorial.pdf

**Attachment:
smime.p7s**

**References**:**[isabelle] Typo in Tutorial?***From:*Andrew Gacek

**Re: [isabelle] Typo in Tutorial?***From:*Tobias Nipkow

**Re: [isabelle] Typo in Tutorial?***From:*Daniel Horne

- Previous by Date: Re: [isabelle] Typo in Tutorial?
- Next by Date: [isabelle] Tactic for Eliminating Parameters Wanted ...
- Previous by Thread: Re: [isabelle] Typo in Tutorial?
- Next by Thread: [isabelle] Trying to instantiate a class
- Cl-isabelle-users February 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list