Email Gateway (Aug 19 2022 at 11:04): Email Gateway (Aug 19 2022 at 11:04):From: "Roger H." <s57076@hotmail.com>
Dear Brian,
thank you for your answer on countable streams.
My main problem is that the Stream theory (and prelude and LNat) , which work perfectly in Isabelle 2011, do not work in 2013 where im writing my new theories.
Some of the problems have to do with countability. Some others are mysterious for me. Thats why i was wondering if you have
a version of the above classes that work in Isabelle 2013, or if you could give me indications how to achieve the adaption, maybe eventual plugin changes .
Many thanks!
Email Gateway (Aug 19 2022 at 11:04):From: Brian Huffman <huffman@in.tum.de>
Could you please tell me what Stream, prelude, and LNat theories you
are using? Are you using files from the Isabelle distribution or from
somewhere else?
Also, please explain what you mean by "do not work in 2013". All
theories bundled with an Isabelle release are tested, and should work.
If problems only arise in connection with your own personal theories,
then you will have to give me more context.
Last updated: Apr 20 2024 at 04:19 UTC