# HG changeset patch # User haftmann # Date 1166426484 -3600 # Node ID 54293c8ea022b77f05731ac29045f9ccc44e2310 # Parent 8750fbc28d5c879d46ffb61ab2d5b07a6fa3e4af added functions tutorial diff -r 8750fbc28d5c -r 54293c8ea022 doc/Contents --- a/doc/Contents Sun Dec 17 22:43:50 2006 +0100 +++ b/doc/Contents Mon Dec 18 08:21:24 2006 +0100 @@ -2,8 +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 + functions Tutorial on Function Definitions + codegen Tutorial on Code Generation axclass Tutorial on Axiomatic Type Classes sugar LaTeX sugar for proof documents ind-defs (Co)Inductive Definitions in ZF