[isabelle] Typo in Tutorial?



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




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