--- a/src/ZF/ex/Primrec0.thy	Fri Oct 22 11:34:41 1993 +0100
+++ b/src/ZF/ex/Primrec0.thy	Fri Oct 22 11:42:02 1993 +0100
@@ -9,6 +9,9 @@
 Nora Szasz, 
 A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
 In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
+
+See also E. Mendelson, Introduction to Mathematical Logic.
+(Van Nostrand, 1964), page 250, exercise 11.
 *)
 
 Primrec0 = ListFn +