doc/Contents
author blanchet
Wed, 01 Jun 2011 19:50:59 +0200
changeset 43139 9ed5d8ad8fa0
parent 41596 e424bc65080d
child 44801 a0459c50cfc9
permissions -rw-r--r--
fixed debilitating translation bug introduced in b6e61d22fa61 -- "equal" and "=" should always have arity 2

Learning and using Isabelle
  tutorial        Tutorial on Isabelle/HOL
  main            What's in Main
  isar-overview   Tutorial on Isar
  locales         Tutorial on Locales
  classes         Tutorial on Type Classes
  functions       Tutorial on Function Definitions
  codegen         Tutorial on Code Generation
  nitpick         User's Guide to Nitpick
  sledgehammer    User's Guide to Sledgehammer
  sugar           LaTeX Sugar for Isabelle documents

Main Reference Manuals
  isar-ref        The Isabelle/Isar Reference Manual
  implementation  The Isabelle/Isar Implementation Manual
  system          The Isabelle System Manual

Old Manuals (outdated)
  intro           Old Introduction to Isabelle
  ref             Old Isabelle Reference Manual
  logics          Isabelle's Logics: overview and misc logics
  logics-HOL      Isabelle's Logics: HOL
  logics-ZF       Isabelle's Logics: FOL and ZF
  ind-defs        (Co)Inductive Definitions in ZF