Yiming Xu (Nov 17 2024 at 18:03): Yiming Xu (Nov 17 2024 at 18:03):It has been 3 months since I (at least supposed to) started work with Isabelle and think I can now use Isabelle to do some simple tasks. As a junior user, I think maybe there will still be some obvious "wrong" way of using Isar stuff, or some folklore among Isar users that I do not know. Here is a proof file that I wrote for formalizing the tree-like model property of modal model theory in Isabelle. It is less than 1000 lines long and this single file is self-contained. I would really appreciate it if some mature users could take a look at it and tell me if there is anything that should be better changed.
I am not asking for a detailed review (I am very aware of the fact that you experts are very busy). I would just like to know if there is something obvious to be improved, even without the knowledge of the proof that I am formalizing. And no emergency at all!
Tree_Like_Property.thy
Last updated: Dec 21 2024 at 16:20 UTC