Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Sat, 20 Nov 1993 20:09:23 +0000
Received: by leopard.cs.byu.edu (1.37.109.7/16.2) id AA16614;
          Sat, 20 Nov 93 13:03:23 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.7/16.2) id AA16610; Sat, 20 Nov 93 13:03:22 -0700
Received: from Maui.CS.UCLA.EDU by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA29748; Sat, 20 Nov 93 12:01:21 -0800
Received: by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.23) id AA10663;
          Fri, 19 Nov 93 22:19:07 -0800
Date: Fri, 19 Nov 93 22:19:07 -0800
From: chou@cs.ucla.edu (Ching-Tsun Chou)
Message-Id: <9311200619.AA10663@maui.cs.ucla.edu>
To: info-hol@cs.uidaho.edu
Subject: HOL for beginners in logic?


Has anyone tried to use HOL in a beginner's logic class?
Or is this a crazy idea?
(By "beginner", I mean CS-major, college freshman.)

- Ching Tsun