added implementation manual;
authorwenzelm
Tue Jan 03 14:07:17 2006 +0100 (2006-01-03)
changeset 185555f216b70215f
parent 18554 bff7a1466fe4
child 18556 dc39832e9280
added implementation manual;
doc/Contents
     1.1 --- a/doc/Contents	Tue Jan 03 13:59:55 2006 +0100
     1.2 +++ b/doc/Contents	Tue Jan 03 14:07:17 2006 +0100
     1.3 @@ -1,19 +1,20 @@
     1.4  Learning Isabelle
     1.5 -  tutorial      Tutorial on Isabelle/HOL
     1.6 -  isar-overview Tutorial on Isar
     1.7 -  locales       Tutorial on Locales
     1.8 +  tutorial        Tutorial on Isabelle/HOL
     1.9 +  isar-overview   Tutorial on Isar
    1.10 +  locales         Tutorial on Locales
    1.11  
    1.12  Reference Manuals
    1.13 -  isar-ref      The Isabelle/Isar Reference Manual
    1.14 -  ref           The Isabelle Reference Manual
    1.15 -  system        The Isabelle System Manual
    1.16 +  isar-ref        The Isabelle/Isar Reference Manual
    1.17 +  implementation  The Isabelle/Isar Implementation
    1.18 +  system          The Isabelle System Manual
    1.19 +  ref             The Isabelle Reference Manual
    1.20  
    1.21  Logics
    1.22 -  logics        Isabelle's Logics: overview and misc logics
    1.23 -  logics-HOL    Isabelle's Logics: HOL
    1.24 -  logics-ZF     Isabelle's Logics: FOL and ZF
    1.25 +  logics          Isabelle's Logics: overview and misc logics
    1.26 +  logics-HOL      Isabelle's Logics: HOL
    1.27 +  logics-ZF       Isabelle's Logics: FOL and ZF
    1.28  
    1.29  Specific Topics
    1.30 -  sugar         LaTeX sugar for proof documents
    1.31 -  axclass       Tutorial on Axiomatic Type Classes
    1.32 -  ind-defs      (Co)Inductive Definitions in ZF
    1.33 +  sugar           LaTeX sugar for proof documents
    1.34 +  axclass         Tutorial on Axiomatic Type Classes
    1.35 +  ind-defs        (Co)Inductive Definitions in ZF