[isabelle] Question about multiset



Hi everyone,
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 Isabelle2011? 
Thanks for the timely help.
Kind regards,
Dongchen 




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