Re: [isabelle] Question about multiset

Hi Dongchen,

> Currently, I am organize my works on finite automata, which uses the
theory of Multiset. It is included in the Isabelle2011. But when I
include this file by using Isabelle2013 with jEdit,  the proofs which
use the rule multiset_def does not work, and the output is Unknown fact
"multiset_def". Does multiset is removed from main.thy of Isabelle2013?
If so, in which file could I find the definition of multiset in

the definition is in


Hope this helps,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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