--- a/src/Doc/Tutorial/document/numerics.tex Fri Jul 04 20:07:08 2014 +0200
+++ b/src/Doc/Tutorial/document/numerics.tex Fri Jul 04 20:18:47 2014 +0200
@@ -20,7 +20,7 @@
infix symbols. Algebraic properties are organized using type classes
around algebraic concepts such as rings and fields;
a property such as the commutativity of addition is a single theorem
-(\isa{add_commute}) that applies to all numeric types.
+(\isa{add.commute}) that applies to all numeric types.
\index{linear arithmetic}%
Many theorems involving numeric types can be proved automatically by
@@ -441,11 +441,11 @@
the two expressions identical.
\begin{isabelle}
a\ +\ b\ +\ c\ =\ a\ +\ (b\ +\ c)
-\rulenamedx{add_assoc}\isanewline
+\rulenamedx{add.assoc}\isanewline
a\ +\ b\ =\ b\ +\ a%
-\rulenamedx{add_commute}\isanewline
+\rulenamedx{add.commute}\isanewline
a\ +\ (b\ +\ c)\ =\ b\ +\ (a\ +\ c)
-\rulename{add_left_commute}
+\rulename{add.left_commute}
\end{isabelle}
The name \isa{add_ac}\index{*add_ac (theorems)}
refers to the list of all three theorems; similarly