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.