# HG changeset patch # User haftmann # Date 1160481552 -7200 # Node ID 981fa0ce23ed7e9b49210c7a7cead90865169af0 # Parent f030835fd9e4db5cd01d99cb172268ba4d411c57 added IsarAdvanced material diff -r f030835fd9e4 -r 981fa0ce23ed doc-src/Contents --- a/doc-src/Contents Tue Oct 10 13:50:33 2006 +0200 +++ b/doc-src/Contents Tue Oct 10 13:59:12 2006 +0200 @@ -1,1 +1,1 @@ -Ref System Logics HOL ZF Inductive AxClass TutorialI IsarOverview IsarRef IsarImplementation Locales LaTeXsugar +Ref System Logics HOL ZF Inductive AxClass TutorialI IsarOverview IsarRef IsarImplementation Locales LaTeXsugar IsarAdvanced/Classes IsarAdvanced/Codegen diff -r f030835fd9e4 -r 981fa0ce23ed doc/Contents --- a/doc/Contents Tue Oct 10 13:50:33 2006 +0200 +++ b/doc/Contents Tue Oct 10 13:59:12 2006 +0200 @@ -2,6 +2,8 @@ tutorial Tutorial on Isabelle/HOL isar-overview Tutorial on Isar locales Tutorial on Locales + classes Tutorial on Haskell-style type classes + codegen Tutorial on code generation axclass Tutorial on Axiomatic Type Classes sugar LaTeX sugar for proof documents ind-defs (Co)Inductive Definitions in ZF