Re: [isabelle] lexical matters



-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

>> ML_val {*
>> cterm_of @{theory} (Free ("a a", @{typ bool}))
>> *}
>>
>> ... prints
>> val it = "a a" : cterm
> 
> This use of cterm_of reminds me of an old trick that has come out of use
> some years ago, because printing with the background theory certificate
> lacks local syntax of the foreground context (local theory or proof body).
> 
> Did you come up with idea yourself, or do we still have it in some old
> manual?

I made it up by myself, being unaware of Syntax.string_of_term. Don't
worry about the manuals.

- -Matthias
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFNM0l7czhznXSdWggRAusXAJ4qB/WlFBQUmfbfXywAVPsIHv8xuQCdGOqO
r6Rt5033J5jZhXciaOPRDek=
=DFfR
-----END PGP SIGNATURE-----





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.