Am 08/05/2012 13:49, schrieb Peter Lammich: > datatype a'::heap linked_list = nil | node 'a "'a linked_list ref"
Actually, I think this does not do what you hope it does, hence the magic is still in there. But Lukas showed me a related defn: datatype 'a ref = Ref nat where 'a is a phantom type but for extra-logical reasons you want to restrict 'a to some type class. Extra-logical reasons can be quite compelling ;-) I'm convinced. Tobias _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
