Re: [isabelle] Error: Non-constructor pattern not allowed in sequential mode

On Thu, 30 Jun 2011, Alexander Krauss wrote:

Or, which is probably easier, you use the "rep_datatype" command to instruct the system to regard the record type you defined as a datatype: After the record definition, do

rep_datatype Foo_ext by (fact Foo.ext_induct) (fact Foo.ext_inject)

Strictly speaking, this exposes implementation details of version 12 of the record package (or is it version 17). It should work for now, but nobody can say when there will be the next change in the internal representation.


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