# HG changeset patch
# User wenzelm
# Date 1333478520 -7200
# Node ID 928cb8b35e6ef71ea0217fae9efeb220b6ae4660
# Parent  8aa23a259ab2eeecf3c76304206c9c9a5c5089d9
formal integration of "prog-prove" manual;
"main" is a reference manual;

diff -r 8aa23a259ab2 -r 928cb8b35e6e doc-src/Dirs
--- 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
diff -r 8aa23a259ab2 -r 928cb8b35e6e doc/Contents
--- 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