Return-Path:
Return-Path: <john.harrison-request@uk.ac.cam.cl>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0)
          id <28728-0@swan.cl.cam.ac.uk>; Fri, 28 Feb 1992 13:03:42 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA04417;
          Fri, 28 Feb 92 04:46:43 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA04288;
          Fri, 28 Feb 92 04:46:28 -0800
Received: from petrel.cl.cam.ac.uk by swan.cl.cam.ac.uk
          with SMTP (PP-6.0) to cl id <28233-0@swan.cl.cam.ac.uk>;
          Fri, 28 Feb 1992 12:48:01 +0000
To: chou@edu.ucla.cs
Cc: info-hol@edu.uidaho.cs.ted, vac@uk.ac.cam.cl
Subject: Re: Strange behavior of quotation parser & a question
In-Reply-To: Your message of Thu, 27 Feb 92 18:04:25 -0800. <9202280204.AA27480@maui.cs.ucla.edu>
Date: Fri, 28 Feb 92 12:47:43 +0000
From: vac@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.248:28.01.92.12.48.33"@cl.cam.ac.uk>



> Sigh!  For some reason I always got into trouble with HOL quotation
> parser.  I have a theory `tla`, which contains (among other things)
> these definitions:

deleted

> It seems that the quotation parser has memory of previous failures.
> The above was performed by an AKCL HOL2.0.

I tryed the same thing and it looks like "and" is redefined and the infix
status no longer holds for the parser!?


#"((A:*->bool) (and:(* -> bool) -> ((* -> bool) -> (* -> bool))) B or C)" ;;
Badly typed application of:  "A"
   which has type:           ":* -> bool"
to the argument term:        "$and"
   which has type:
    ":(* -> bool) -> ((* -> bool) -> (* -> bool))"

evaluation failed     mk_comb in quotation

#"and (A:*->bool) B";;
"A and B" : term

Victor.