New/updated information files

3 files changed, 37 insertions, 4 deletions

diff --git a/isar/BUGS b/isar/BUGS
new file mode 100644
index 00000000..baddf520
--- /dev/null
+++ b/isar/BUGS
@@ -0,0 +1,9 @@
+-*- mode:outline -*-
+
+* Isabelle/Isar Proof General Bugs
+
+See also ../BUGS for generic bugs.
+
+Nothing specific here, check isa/BUGS for some issues that may apply
+to Isar as well.
+
diff --git a/isar/README b/isar/README
new file mode 100644
index 00000000..f9d0e689
--- /dev/null
+++ b/isar/README
@@ -0,0 +1,25 @@
+Isabelle/Isar Proof General
+
+Written by Markus Wenzel
+
+$Id$
+
+Status:		   supported
+Maintainer:	   Markus Wenzel
+Isabelle version:  99
+Isar homepage:	   http://isabelle.in.tum.de/Isar/
+
+========================================
+
+Isabelle/Isar Proof General has full support for multiple file
+scripting, with dependencies between theories communicated between
+Isabelle and Proof General.  
+
+There is proper support for X Symbol, using the Isabelle print mode
+for X Symbol tokens.  Many Isabelle theories have X Symbol syntax
+already defined and it's easy to add to your own theories.
+
+There is no support for proof by pointing yet, and no tags program.
+
+The script `interface' and file 'interface-setup.el' are used to start
+Isabelle Proof General via the 'Isabelle' shell command.  
diff --git a/isar/todo b/isar/todo
index a7ba9473..19258d94 100644
--- a/isar/todo
+++ b/isar/todo
@@ -1,9 +1,8 @@
 -*- mode:outline -*-
 
-* See also ../todo for generic things to do, priority codes.
-
 * Things to do for Isabelle/Isar
-================================
 
-C Combine with isa/ to get single Isabelle PG instance, maybe?
+See also ../todo for generic things to do, priority codes.
+
+** C Combine with isa/ to get single Isabelle PG instance, maybe?