# HG changeset patch
# User wenzelm
# Date 1136293637 -3600
# Node ID 5f216b70215f1ad7e72fb2156425b84bfc50c832
# Parent  bff7a1466fe455bbfbeefc4a5e31b00c1f8b9714
added implementation manual;

diff -r bff7a1466fe4 -r 5f216b70215f doc/Contents
--- a/doc/Contents	Tue Jan 03 13:59:55 2006 +0100
+++ b/doc/Contents	Tue Jan 03 14:07:17 2006 +0100
@@ -1,19 +1,20 @@
 Learning Isabelle
-  tutorial      Tutorial on Isabelle/HOL
-  isar-overview Tutorial on Isar
-  locales       Tutorial on Locales
+  tutorial        Tutorial on Isabelle/HOL
+  isar-overview   Tutorial on Isar
+  locales         Tutorial on Locales
 
 Reference Manuals
-  isar-ref      The Isabelle/Isar Reference Manual
-  ref           The Isabelle Reference Manual
-  system        The Isabelle System Manual
+  isar-ref        The Isabelle/Isar Reference Manual
+  implementation  The Isabelle/Isar Implementation
+  system          The Isabelle System Manual
+  ref             The Isabelle Reference Manual
 
 Logics
-  logics        Isabelle's Logics: overview and misc logics
-  logics-HOL    Isabelle's Logics: HOL
-  logics-ZF     Isabelle's Logics: FOL and ZF
+  logics          Isabelle's Logics: overview and misc logics
+  logics-HOL      Isabelle's Logics: HOL
+  logics-ZF       Isabelle's Logics: FOL and ZF
 
 Specific Topics
-  sugar         LaTeX sugar for proof documents
-  axclass       Tutorial on Axiomatic Type Classes
-  ind-defs      (Co)Inductive Definitions in ZF
+  sugar           LaTeX sugar for proof documents
+  axclass         Tutorial on Axiomatic Type Classes
+  ind-defs        (Co)Inductive Definitions in ZF