[isabelle] quickchecking lemma with types defined by typedecl



Hi,

I’ve got an error message when I quickcheck a lemma with types defined by typedecl. A dummy example to illustrate the problem:

	typedecl "S"
	consts "s" :: "S"
	consts "l" :: "S set"

	lemma "s : l"
	  quickcheck

What do I miss here ? Thanks in advance.

regrads,
Yuhui
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.


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