added implementation manual;
authorwenzelm
Tue, 03 Jan 2006 14:07:17 +0100
changeset 18555 5f216b70215f
parent 18554 bff7a1466fe4
child 18556 dc39832e9280
added implementation manual;
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