[isabelle] Records with String types


I am a new Isabelle user. I have some questions regarding the usage of string types with records. 

Can I define something like this as a record definition
record class = 
className :: string
classType :: string

should the same be defined using 'char' data type. If the above
definition is allowed and correct then how can this be 'concretely'
defined. Basically, how can I define a constant of type 'class'? Can
someone please provide some pointers for any examples that uses string
types in records? 

Thanks for the help,

Looking for last minute shopping deals?  
Find them fast with Yahoo! Search.  http://tools.search.yahoo.com/newsearch/category.php?category=shopping

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