Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Thu, 9 Dec 1993 15:35:14 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA26493; Thu, 9 Dec 1993 08:23:32 -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.8/16.2) id AA26489; Thu, 9 Dec 1993 08:23:01 -0700 Received: from iraun1.ira.uka.de by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA02975; Thu, 9 Dec 1993 07:19:32 -0800 Received: from ira.uka.de by iraun1.ira.uka.de id <08328-0@iraun1.ira.uka.de>; Thu, 9 Dec 1993 16:18:51 +0100 Received: from ira.uka.de by i80fs2.ira.uka.de id <14868-0@i80fs2.ira.uka.de>; Thu, 9 Dec 1993 16:17:44 +0100 Date: Thu, 9 Dec 93 16:17:43 EST From: reetz To: info-hol@cs.uidaho.edu Subject: load_theory,print_theory and new_parent in hol90.6 Message-Id: <"i80fs2.ira.870:09.11.93.15.17.58"@ira.uka.de> Dear all, I'm totally confused about using my own theories in hol90.6. (new_parent "my_own") fails after starting hol90.6. But using (print_theory "my_own") and than using (new_parent "my_own") does work. Strange things does happen with load_theory, too. sometimes it works, sometimes not. I tried hard to get a reproductive error, but it seemed ``randomly''. (my theory path is set correctly) So, could somebody please explain me everything around dependency of theories within hol90.6 in respect of own theories? Maybe it will help... thanks in advance :) (*****************************************************************************) (* *) (* Ralf Reetz SFB 358 of the german research society (DFG) *) (* reetz@ira.uka.de University of Karlsruhe, Germany *) (* *) (* "we prove around in a ring and suppose, *) (* the goal sits right in the middle and knows." *) (* *) (*****************************************************************************)