[opentheory-users] the Unwanted namespace

[Michael Norrish]

On 7/12/11 6:47 PM, Ramana Kumar wrote:
> On Dec 6, 2011 11:02 PM, "Michael Norrish" <Michael.Norrish at nicta.com.au
> <mailto:Michael.Norrish at nicta.com.au>> wrote:
>>
>> I think the mistake here is mapping the Abbrev constant to Unwanted.
>  I'd say it was probably worth preserving.
> 
> Why? What does it mean outside of HOL4?

Nothing particularly.  But I want to use opentheory as a storage
mechanism for HOL4 theories, and so the technology needs to be faithful
to what is in the HOL4 theories.  But I admit I may have misunderstood
the issue here.  In particular, I'd be surprised if Abbrev actually
appears in any theory's exports except for the definition and that
forall-rewrite.

Michael


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 551 bytes
Desc: OpenPGP digital signature
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20111207/db0c9a47/attachment.pgp>