Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2);
          Thu, 8 Oct 1992 20:18:03 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA06432;
          Thu, 8 Oct 92 12:04:39 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from air15.larc.nasa.gov by ted.cs.uidaho.edu (16.6/1.34) id AA06426;
          Thu, 8 Oct 92 12:04:31 -0700
Received: by air15.larc.nasa.gov (5.65.1/lanleaf2.4) id AA00555;
          Thu, 8 Oct 92 15:03:59 -0400
Message-Id: <9210081903.AA00555@air15.larc.nasa.gov>
Date: Thu, 8 Oct 92 15:03:59 -0400
From: Victor "A." Carreno <vac@gov.nasa.larc.air16>
To: wishnu@nl.ruu.cs
Subject: Re: QUESTION: hanging by defining tactic.
In-Reply-To: Mail from 'Wishnu Prasetya <wishnu@cs.ruu.nl>' dated: Thu, 8 Oct 92 19:48:20 MET
Cc: info-hol@edu.uidaho.cs.ted


This may be good news or bad news, but your code runs OK in HOL2:

  let INFER_ASMN_TAC n inf_rule (asml,g) =
     ASSUME_TAC (inf_rule (ASSUME (el n asml))) (asml,g) ;;

INFER_ASMN_TAC = - : (int -> (thm -> thm) -> tactic)

  letrec last l = last (tl l) ? hd l ? failwith `last on empty list` ;;

last = - : (* list -> *)

  let IMP_LEFT_RULE trm thm = 
     let th1 = SPEC_ALL thm in
     let th2 = UNDISCH th1 in
     let th3 = CONJUNCT1 th2 in
     let th4 = DISCH (last (hyp th3)) th3  in
     GEN trm th4 ;;

IMP_LEFT_RULE = - : (term -> thm -> thm)

  let MYTAC th = 
        INFER_ASMN_TAC 1 (IMP_LEFT_RULE "p':*->bool")
        THEN (IMP_RES_TAC th) ;;

MYTAC = - : thm_tactic


Victor.