Rob,
val it = () : unit
val it = () : unit
=== ProofPower 2.8.1a10 [HOL Database]
=== Copyright (C) Lemma 1 Ltd. 2000-2008
Database name:
:) signature ZTypesAndTermsSupport =
sig
val ¶‰1‰s_bname :
string list -> string list -> string
val ¶‰1‰s_bterm :
(string * TYPE) list -> (string * TYPE) list -> TERM
val ¶‰1‰s_btype :
(string * TYPE) list -> (string * TYPE) list -> TYPE
val ¶‰1_bname : string list -> string
val ¶‰1_bterm : (string * TYPE) list -> TERM
val ¶‰1_btype : (string * TYPE) list -> TYPE
val ¶‰s_bname : string list -> string list -> string
val ¶‰s_bterm :
(string * TYPE) list -> (string * TYPE) list -> TERM
And it goes till the end as I attached before.
Artur
2008/12/20 Rob Arthan <[email protected]>
> Artur,
>
> What do the top 10 lines of src/dtd048.ldd say?
>
> Regards,
>
> Rob.
>
> On Saturday 20 Dec 2008 12:53 pm, Artur Oliveira Gomes wrote:
> > Rob,
> >
> > > The signature should have been defined when dtd048.sml was compiled.
> The
> > > log
> > > from compiling dtd048.sml should be in src/dtd048.ldd, so do you have
> > > that file? And what does it say?
> >
> > val unpack_ident : string -> string * string
> > val val_numeral : string -> int
> > val val_set_ident : string list -> string
> > val z_sig_order : string -> string -> int
> > end
> > val it = () : unit
> > +++ Compiled dtd048.sml: OK (Compilation Run Complete) +++
> > Exception Fail * The database name has not been set [save_and_exit.36010]
> *
> > raised
> >
> > :) End of input to use_terminal. Quit.
>
>
--
Artur Oliveira Gomes
_______________________________________________
Proofpower mailing list
[email protected]
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
