Email Gateway (Aug 18 2022 at 12:31): Email Gateway (Aug 18 2022 at 12:31):From: Mike Aizatsky <mike.aizatsky@gmail.com>
Hi!
I'm currently working through isabelle tutorial, and while all
definition stuff is quite understandable, there's one area which is a
complete magic for me: choosing what to type in "apply (<tac>)" to
prove the theorem. Are there better texts to grasp this? Or should I
read the tutorial and fight with my theorems till I win?
Right now I'm trying to prove some basic facts about graphs and it's
really, really painful to move forward. Is it possible for some more
advanced users of isabelle to take a look at what I'm doing and push
me in the right direction? Can same things be expressed more easily in
isabelle? I'm attaching the file I'm working on.
graph2.thy
Last updated: Nov 21 2024 at 12:39 UTC