[isabelle] Instantiation on records



Dear all,

I'm currently struggeling with making record-types an instance of some
class. I can't find a way of getting hold of the underlying type:

record test =
  bla :: int

instantiation "test" :: linorder
begin -- "yields: Bad type name"

instantiation "test_scheme" :: (unit) linorder
begin -- "yields: Bad type name"

instantiation "(| bla :: int |)" :: linorder
begin -- "yields: Undeclared type constructor"



Is it somehow possible to do this? Or should I use explicit 'datatype'
or tuple constructions instead?

Thanks,
- René
-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift



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