Return-Path: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) id <19033-0@swan.cl.cam.ac.uk>; Mon, 1 Jun 1992 21:47:04 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA07452; Mon, 1 Jun 92 13:33:58 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA07448; Mon, 1 Jun 92 13:33:52 -0700 Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 5.61b+YP/3.13) id AA29394; Mon, 1 Jun 92 13:34:18 -0700 Message-Id: <9206012034.AA29394@maui.cs.ucla.edu> To: info-hol@edu.uidaho.cs.ted Cc: chou@edu.ucla.cs Subject: CASES_THENL and DISJ_CASES_THENL Date: Mon, 01 Jun 92 13:34:16 PDT From: chou@edu.ucla.cs Has anyone used CASES_THENL and DISJ_CASES_THENL? If so, could you send me an example or two? I'm writing a paper on how to do interactive theorem proving with theorem continuation functions but I don't know any good example of the use of CASES_THENL and DISJ_CASES_THENL. Many thanks in advance! Cheers, Ching-Tsun Chou