Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <17672-0@swan.cl.cam.ac.uk>; Thu, 14 May 1992 01:31:34 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA09237;
          Wed, 13 May 92 17:08:54 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from Ewa.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA09233;
          Wed, 13 May 92 17:08:35 -0700
Received: from LocalHost by ewa.cs.ucla.edu (Sendmail 5.61a+YP/2.27) id AA15050;
          Wed, 13 May 92 17:08:44 -0700
Message-Id: <9205140008.AA15050@ewa.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Cc: toal@edu.ucla.cs
Subject: Ackermann's function
Date: Wed, 13 May 92 17:08:42 PDT
From: toal@edu.ucla.cs


The footnote on p. 180 of DESCRIPTION states that Ackermann's function
can be defined by primitive recursion in HOL.  Just curious how.

Ray Toal