Lu Zhao wrote:
> Hi,
>
> When I use match_term with some types unspecified, HOL always generates
> a message similar to the following:
>
> <>
>
> Is there a way to depress the message so that I don't have to see a long
> list of messages. Specifying the types is not a good option since the
>
Hi Lu,
That message comes from the parser, when
unconstrained type variables remain after
type inference. So it seems that you are making
an invocation
match_term `` ...`` `` ... ``;
where one or both of the terms involved are
being parsed. If you don't want to see any
messages you can
OPEN POSITION AT ETH ZURICH
Usage Control in Ubiquitous Communication (UC^2)
The research group headed by Prof. David Basin at the Swiss Federal
Institute of Technology, Zurich (ETH Zurich) has an open position for
a PhD student or a postdoctoral researcher.
T
Call For Participation
22nd IEEE Computer Security Foundations Symposium (CSF)
Port Jefferson, NY, USA
July 8-10, 2009
http://www.cs.stonybrook.edu/csf09/
* Early registration ends on June 3. **
Hi,
When I use match_term with some types unspecified, HOL always generates
a message similar to the following:
<>
Is there a way to depress the message so that I don't have to see a long
list of messages. Specifying the types is not a good option since the
matched terms have multiple types a
%%
SCSS 2009
TUNISIA - JAPAN WORKSHOP ON
SYMBOLIC COMPUTATION IN SOFTWARE SCIENCE
September 22-24, 2009
Gammarth, Tunisia
http://www2.score.cs.tsukuba.ac.jp/scssWorkshop/index.html
%%
IMPORTANT DATES
===
Abstract submission: Ma
