Re: [isabelle] Records with String types



On Wed, 20 Feb 2008, Rajesh Karunamurthy wrote:

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

Yes, here is an example:

record "class" = 
  class_name :: string
  class_type :: string

definition "my_class = (| class_name = ''foo'', class_type = ''bar'' |)"


	Makarius





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