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, 3 Dec 1992 12:55:23 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA20456;
          Thu, 3 Dec 92 04:42:44 -0800
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 AA20451;
          Thu, 3 Dec 92 04:42:28 -0800
Received: by infix.cs.ruu.nl id AA01381 (5.65c/IDA-1.4.4 
          for info-hol@ted.cs.uidaho.edu); Thu, 3 Dec 1992 13:41:46 +0100
From: Wishnu Prasetya <wishnu@nl.ruu.cs>
Message-Id: <199212031241.AA01381@infix.cs.ruu.nl>
Subject: HELP: RES_TAC
To: info-hol@edu.uidaho.cs.ted (hol mailing list)
Date: Thu, 3 Dec 92 13:41:45 MET
X-Mailer: ELM [version 2.3 PL11]

Hi there!

Just a small question. Any idea why RES_TAC does not create any new assumption
in the case below? I would say it should.

   OK..
   "WELL_FOUNDED(R 0)"
       [ "0 < n \/ (0 = n) ==> WELL_FOUNDED(R 0)" ]
       [ "0 < n \/ (0 = n)" ]

   () : void

   #e RES_TAC;;
   OK..
   "WELL_FOUNDED(R 0)"
       [ "0 < n \/ (0 = n) ==> WELL_FOUNDED(R 0)" ]
       [ "0 < n \/ (0 = n)" ]

   () : void

   #

Thanks for any hints.

-Wishnu Prasetya-

--