[isabelle] Browsing finished theories in Isabelle/jEdit



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.

Attachment: signature.asc
Description: PGP signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.