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
Isabelle2011?

the definition is in

	~~/src/HOL/Library/Multiset.thy

Hope this helps,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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