[MC] ================================================ AMAST Links 02 03

       Introduction to Theorem Proving, Using Isabelle (Course)
		 12-14 July 1995, Cambridge, England

   The full version of this announcement is available at URL:
   http://www.cs.utwente.nl/data/amast/links/v02/i03/full/AC0203MC.txt

  Immediately prior to Mathematics of Program Construction (MPC '95).
  *Full information:* available via the WWW page at URL:
http://www.cl.cam.ac.uk/users/lcp/isabelle-course.html
  *Topics* The course uses lectures and practical sessions to teach
students how to use the Isabelle system to perform proofs in
higher-order logic.  Main points:
 o  Single-step proof checking.	 Forward and backward proof.
 o  Declaring types and constants.  Quantifier reasoning.  
 o  Higher-Order Logic in Isabelle.  Advanced proof tools.
  *Lecturer*  Lawrence C Paulson, the originator of Isabelle.
  *Cost* 650 pounds sterling (350 pounds for academics) plus
accommodation.
  *Technical Correspondence*
   Lawrence C Paulson, Computer Laboratory,
   Pembroke Street, Cambridge CB2 3QG, England. E-mail lcp@cl.cam.ac.uk
  *Administrative Correspondence*
   The Registration Administrator, Programme for Industry
   1 Trumpington St, Cambridge CB2 1QA, England.
   Tel +44 (0)1223 302233.  E-mail: rjs1008@cus.cam.ac.uk