# HG changeset patch
# User aspinall
# Date 1128095538 -7200
# Node ID 9c7fc0d5cf84399d5273430984387d1fda0adb6b
# Parent  636becdc3cccffae93df68282216b7c39137170e
Add helpdocs and welcomemsg here instead of hard wiring in proof_general.ML.

diff -r 636becdc3ccc -r 9c7fc0d5cf84 lib/ProofGeneral/pgip_isar.xml
--- a/lib/ProofGeneral/pgip_isar.xml	Fri Sep 30 17:33:22 2005 +0200
+++ b/lib/ProofGeneral/pgip_isar.xml	Fri Sep 30 17:52:18 2005 +0200
@@ -15,6 +15,36 @@
 -->
 
 <displayconfig>
+
+  <!-- basic prover information and pointers to documentation -->
+
+  <welcomemsg>Welcome to Isabelle/Isar 2005.</welcomemsg>
+
+  <helpdoc name="Isabelle/HOL Tutorial" 
+	   descr="A gentle introduction to Isabelle/HOL"
+           url="http://isabelle.in.tum.de/dist/Isabelle/doc/tutorial.pdf"
+  >tutorial</helpdoc>
+  <helpdoc name="Isabelle HOL Logic Reference" 
+	   descr="The Isabelle HOL Logic in detail"
+           url="http://isabelle.in.tum.de/dist/Isabelle/doc/logics-HOL.pdf"
+  >logics-HOL</helpdoc>
+  <helpdoc name="Isar Tutorial" 
+	   descr="An Introduction to the Isar proof language"
+           url="http://isabelle.in.tum.de/dist/Isabelle/doc/isar-overview.pdf"
+  >isar-overview</helpdoc>
+  <helpdoc name="Isabelle/Isar Reference" 
+	   descr="Reference Manual for Isabelle/Isar"
+           url="http://isabelle.in.tum.de/dist/Isabelle/doc/isar-ref.pdf"
+  >isar-ref</helpdoc>
+  <helpdoc name="Isabelle Reference manual"
+	   descr="Reference Manual for Isabelle"
+           url="http://isabelle.in.tum.de/dist/Isabelle/doc/ref.pdf"
+  >ref</helpdoc>
+  <helpdoc name="Isabelle System manual"
+	   descr="System Manual: interfaces, output, building logics."
+           url="http://isabelle.in.tum.de/dist/Isabelle/doc/system.pdf"
+  >system</helpdoc>
+
   <!-- objtypes -->
   <objtype name="toplevel" descr="top-level context (PGIP internal)">
   <contains objtype="theory"/>