*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Typo in Tutorial?*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 25 Feb 2015 13:10:39 +0100*In-reply-to*: <CAHgzvFjLRE0gYG-rvAYPcnnyEw1gZxuSnUGzStrVLvyQ1X+KbQ@mail.gmail.com>*References*: <CAHgzvFjLRE0gYG-rvAYPcnnyEw1gZxuSnUGzStrVLvyQ1X+KbQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.9; rv:31.0) Gecko/20100101 Thunderbird/31.4.0

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**

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

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

- Previous by Date: Re: [isabelle] Measure definition on streams
- Next by Date: [isabelle] Trying to instantiate a class
- Previous by Thread: [isabelle] Typo in Tutorial?
- Next by Thread: Re: [isabelle] Typo in Tutorial?
- 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