diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/NewDoc.texi | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/doc/NewDoc.texi b/doc/NewDoc.texi index 08cb225a..7c59cb57 100644 --- a/doc/NewDoc.texi +++ b/doc/NewDoc.texi @@ -698,6 +698,23 @@ At present there is no easy way to get around this. @node Isabelle specific commands @section Isabelle specific commands +@unnumberedsubsec Associated files +@cindex Associated files + +In Isabelle proofscript mode, @kbd{C-c C-o} (@code{thy-find-other-file}) +finds and switches to the associated theory file, that is, the file with +the same base name but extension @file{.thy} swapped for @file{.ML}. + +The same function (and keybinding) switches back to an ML file from the +theory file. + +@deffn Command thy-find-other-file +Find and switch to the associated ML file (when editing a theory file) +or theory file (when editing an ML file). +@end deffn + + + @node Isabelle customizations @section Isabelle customizations |