Email Gateway (Aug 19 2022 at 12:35): Email Gateway (Aug 19 2022 at 12:35):From: jiangdc <jiangdc@nlsde.buaa.edu.cn>
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
Email Gateway (Aug 19 2022 at 12:40):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc
Email Gateway (Aug 19 2022 at 12:49):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Dongchen,
you should replace any occurent of Cset.set by plain set in
Isabelle2013. Cset.set was just an auxiliary type and is now gone for good.
Hope this helps,
Florian
signature.asc
Last updated: Apr 18 2024 at 20:16 UTC