formal integration of "prog-prove" manual;
"main" is a reference manual;

--- a/doc-src/Dirs	Tue Apr 03 20:37:52 2012 +0200
+++ b/doc-src/Dirs	Tue Apr 03 20:42:00 2012 +0200
@@ -1,1 +1,1 @@
-Intro Ref System Logics HOL ZF Inductive TutorialI IsarOverview IsarRef IsarImplementation Locales LaTeXsugar Classes Codegen Functions Nitpick Main Sledgehammer
+Intro Ref System Logics HOL ZF Inductive TutorialI IsarOverview IsarRef IsarImplementation Locales LaTeXsugar Classes Codegen Functions Nitpick Main Sledgehammer ProgProve

--- a/doc/Contents	Tue Apr 03 20:37:52 2012 +0200
+++ b/doc/Contents	Tue Apr 03 20:42:00 2012 +0200
@@ -1,6 +1,6 @@
 Miscellaneous tutorials
   tutorial        Tutorial on Isabelle/HOL
-  main            What's in Main
+  prog-prove      Programming and Proving in Isabelle/HOL
   isar-overview   Tutorial on Isar
   locales         Tutorial on Locales
   classes         Tutorial on Type Classes
@@ -10,7 +10,8 @@
   sledgehammer    User's Guide to Sledgehammer
   sugar           LaTeX Sugar for Isabelle documents
 
-Main Reference Manuals
+Reference Manuals
+  main            What's in Main
   isar-ref        The Isabelle/Isar Reference Manual
   implementation  The Isabelle/Isar Implementation Manual
   system          The Isabelle System Manual