On Fri, 13 May 2011, [email protected] wrote:
Is there a way to create a type out of a string? I know there's the
antiquotation @{type...}, but if the string was stored as a value, eg,
val str = "nat => nat", @{type str} doesn't seem to work.
Maybe you mean Syntax.read_typ, although your description sounds quite
differently. These parse/check/read operations internalized
specifications given in end-user syntax, so you don't "store" such
strings.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
