[isabelle] Question about multiset
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and