doc/Contents
changeset 20831 4981b56f8cde
parent 18555 5f216b70215f
child 20950 981fa0ce23ed
     1.1 --- a/doc/Contents	Mon Oct 02 21:30:05 2006 +0200
     1.2 +++ b/doc/Contents	Mon Oct 02 23:00:45 2006 +0200
     1.3 @@ -1,20 +1,16 @@
     1.4 -Learning Isabelle
     1.5 +Learning and using Isabelle
     1.6    tutorial        Tutorial on Isabelle/HOL
     1.7    isar-overview   Tutorial on Isar
     1.8    locales         Tutorial on Locales
     1.9 +  axclass         Tutorial on Axiomatic Type Classes
    1.10 +  sugar           LaTeX sugar for proof documents
    1.11 +  ind-defs        (Co)Inductive Definitions in ZF
    1.12  
    1.13  Reference Manuals
    1.14    isar-ref        The Isabelle/Isar Reference Manual
    1.15    implementation  The Isabelle/Isar Implementation
    1.16    system          The Isabelle System Manual
    1.17    ref             The Isabelle Reference Manual
    1.18 -
    1.19 -Logics
    1.20    logics          Isabelle's Logics: overview and misc logics
    1.21    logics-HOL      Isabelle's Logics: HOL
    1.22    logics-ZF       Isabelle's Logics: FOL and ZF
    1.23 -
    1.24 -Specific Topics
    1.25 -  sugar           LaTeX sugar for proof documents
    1.26 -  axclass         Tutorial on Axiomatic Type Classes
    1.27 -  ind-defs        (Co)Inductive Definitions in ZF