read : string -> tag
STRUCTURE
Tag
SYNOPSIS
Make a tag suitable for use by mk_oracle_thm.
DESCRIPTION
In order to construct a tag usable by mk_oracle_thm, one uses read, which takes a string and makes it into a tag.
FAILURE
The string must be an alphanumeric, i.e., start with an alphabetic character and thereafter consist only of alphabetic or numeric characters.
EXAMPLE
- Tag.read "Shamboozled";
> val it = Kerneltypes.TAG(["Shamboozled"], []) : tag

SEEALSO
mk_oracle_thm, tag
HOL  Kananaskis-13