# HG changeset patch # User clasohm # Date 816438501 -3600 # Node ID a60d1abb06c0a865ebfb3aaec6e9c18e90af59c7 # Parent 70ee8d7b22330d42ff1d521fa9f8229913316b0a added link to README.html or README diff -r 70ee8d7b2233 -r a60d1abb06c0 src/Pure/Thy/thy_read.ML --- a/src/Pure/Thy/thy_read.ML Wed Nov 15 13:27:57 1995 +0100 +++ b/src/Pure/Thy/thy_read.ML Wed Nov 15 13:28:21 1995 +0100 @@ -1067,7 +1067,7 @@ val subdir = relative_path base_path (!index_path); in output (out, "Isabelle/" ^ subdir ^ "\n\ - \

Isabelle/" ^ subdir ^ "

\n\ + \

Isabelle/" ^ subdir ^ "

\n\ \The name of every theory is linked to its theory file
\n\ \\\/ stands for subtheories (child theories)
\n\ @@ -1075,8 +1075,13 @@ \\" ALT = /\\> stands for supertheories (parent theories)\n\ \

\ - \Back to the index of Isabelle logics.\n


" ^ - main_entries theories (space_explode "/" base_path) ^ + \Back to the index of Isabelle logics.\n" ^ + (if file_exists "README.html" then + "
View the ReadMe file.\n" + else if file_exists "README" then + "
View the ReadMe file.\n" + else "") ^ + "
" ^ main_entries theories (space_explode "/" base_path) ^ "\n"); close_out out end;