Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Tue, 20 Apr 1993 17:39:30 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA16683;
          Tue, 20 Apr 93 09:22:32 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from iraun1.ira.uka.de by ted.cs.uidaho.edu (16.6/1.34) id AA16678;
          Tue, 20 Apr 93 09:22:14 -0700
Message-Id: <9304201622.AA16678@ted.cs.uidaho.edu>
Received: from ira.uka.de by iraun1.ira.uka.de with SMTP (PP) 
          id <29881-0@iraun1.ira.uka.de>; Tue, 20 Apr 1993 16:06:47 +0200
Date: Tue, 20 Apr 93 16:07:44 MET DST
From: reetz <reetz@ira.uka.de>
To: info-hol@ted.cs.uidaho.edu
Subject: print_theory in HOL90.5

Dear all,
I have the following problem with HOL90.5:
using print_theory "pair", I don't get the
theorem PAIR_EQ, with I'll get with
theorem "pair" "PAIR_EQ"?
Is there a problem with installation or
is there an error with print_theory?

- print_theory "pair";
Theory: pair
 
Parents:
    bool
 
Type constants:
    prod 2
 
Term constants:
    MK_PAIR (Prefix)   :'a -> 'b -> 'a -> 'b -> bool
    IS_PAIR (Prefix)   :('a -> 'b -> bool) -> bool
    REP_prod (Prefix)   :'a # 'b -> 'a -> 'b -> bool
    , (Infix 50)   :'a -> 'b -> 'a # 'b
    FST (Prefix)   :'a # 'b -> 'a
    SND (Prefix)   :'a # 'b -> 'b
    UNCURRY (Prefix)   :('a -> 'b -> 'c) -> 'a # 'b -> 'c
    CURRY (Prefix)   :('a # 'b -> 'c) -> 'a -> 'b -> 'c
 
Axioms:
    
 
Definitions:
    MK_PAIR_DEF |- !x y. MK_PAIR x y = (\a b. (a = x) /\ (b = y))
    IS_PAIR_DEF |- !p. IS_PAIR p = (?x y. p = MK_PAIR x y)
    prod_TY_DEF |- ?rep. TYPE_DEFINITION IS_PAIR rep
    REP_prod
    |- REP_prod =
       (@rep.
         (!p' p''. (rep p' = rep p'') ==> (p' = p'')) /\
         (!p. IS_PAIR p = (?p'. p = rep p')))
    COMMA_DEF |- !x y. (x,y) = (@p. REP_prod p = MK_PAIR x y)
    FST_DEF |- !p. FST p = (@x. ?y. MK_PAIR x y = REP_prod p)
    SND_DEF |- !p. SND p = (@y. ?x. MK_PAIR x y = REP_prod p)
    UNCURRY_DEF |- !f x y. UNCURRY f (x,y) = f x y
    CURRY_DEF |- !f x y. CURRY f x y = f (x,y)
 
Theorems:
    PAIR |- !x. (FST x,SND x) = x
    FST |- !x y. FST (x,y) = x
    SND |- !x y. SND (x,y) = y
    val it = () : unit
- theorem "pair" "PAIR_EQ";
val it = |- ((x,y) = (a,b)) = (x = a) /\ (y = b) : thm
-


Ralf 

reetz@ira.uka.de