I want to use Isabelle to better understand the Knaster-Tarski fixpoint theorem. So, I fire up Isabelle/jEdit and use the "Search in Directory..." feature to look for "Knaster-Tarski" (BTW, it would be great if the directory list in the dialog box automatically included $ISABELLE_HOME). I quickly find that there is a well explained example ($ISABELLE_HOME/src/HOL/Isar_Examples/Knaster_Tarski.thy; thanks Makarius). Now, looking at the theorem, I want to know the exact definition of a complete lattice, so I COMMAND/CTRL-click on "complete_lattice". The Complete_Lattices.thy file opens at the correct position but is not processed (everything is pink) due to the error "Cannot update finished theory". This means, in particular, that I cannot continue COMMAND/CTRL-clicking to follow the definitions further. Thus this naive question from someone who no longer uses Isabelle every day (sniff): is there a better way of read-only browsing the contents of an open session in Isabelle/jEdit? I know that the theory files can be browsed online at http://isabelle.in.tum.de/dist/library/HOL/HOL-Isar_Examples/Knaster_Tarski.html but there I cannot click on elements to see their definitions, nor use the other great features of Isabelle and Isabelle/jEdit. I also know that, on a Mac, I can launch Isabelle/jEdit with /Applications/Isabelle2016-1.app/Isabelle/bin/isabelle jedit -l Pure and then open /Applications/Isabelle2016-1.app/Isabelle/src/HOL/Main.thy to browse the theories, but a slip on the keyboard risks a rebuild, and I thought I would ask the question anyway for those who are even less experienced than me. This question is also something I have wondered about when teaching Isabelle. I explain to students that they can COMMAND/CTRL-click to follow definitions to learn about the underlying libraries, but they quickly come face-to-face with the same issue. Tim.
Description: PGP signature