From bd63ee707863cec05c08e3e5758ac58bb88ae406 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 4 Nov 1998 13:57:10 +0000
Subject: Added key binding to switch between theory and ML files.

---
 doc/NewDoc.texi | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'doc')

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
 
-- 
cgit v1.2.3