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 19:09:44 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA06286;
          Thu, 8 Oct 92 10:54:43 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from infix.cs.ruu.nl by ted.cs.uidaho.edu (16.6/1.34) id AA06280;
          Thu, 8 Oct 92 10:54:18 -0700
Received: by infix.cs.ruu.nl id AA17838 (5.65c/IDA-1.4.4 
          for info-hol@ted.cs.uidaho.edu); Thu, 8 Oct 1992 18:53:19 +0100
From: Wishnu Prasetya <wishnu@nl.ruu.cs>
Message-Id: <199210081753.AA17838@infix.cs.ruu.nl>
Subject: QUESTION: hanging by defining tactic.
To: info-hol@edu.uidaho.cs.ted (hol mailing list)
Date: Thu, 8 Oct 92 18:53:19 MET
X-Mailer: ELM [version 2.3 PL11]

Hi,

I'm using HOL 1.xx (yes... still using that old version :-( ), and trying
to define theorem-tactic MYTAC as follows:

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

where:

  INFER_ASMN_TAC n RULE 
     is a tactic that applies infference rule RULE to n-th assumption 
     then adds the result to the assumptions list

  IMP_LEFT_RULE term
     just some self-defined infference rule

  
but strangely my HOL then just hangs there. Any idea why?? The
definition seems innocent to me: the type is OK:

#INFER_ASMN_TAC;;
- : (int -> (thm -> thm) -> tactic)

#IMP_LEFT_RULE ;;
- : (term -> thm -> thm)

so above is supposed to be a simple tactics composition, but why the
HOL hangs?


Kindly thank you for any hint on this. 


My best regard,

Wishnu Prasetya