doc/Contents
author Walther Neuper <neuper@ist.tugraz.at>
Wed, 08 Sep 2010 17:20:03 +0200
branchisac-update-Isa09-2
changeset 37994 eb4c556a525b
parent 36922 15d9f4373f78
child 41844 e424bc65080d
permissions -rw-r--r--
tuned

src/Knowledge + test/Knowledge:
find . -type f -exec sed -i s/"f_\""/"f_f\""/g {} \;
find . -type f -exec sed -i s/"f_,"/"f_f,"/g {} \;
find . -type f -exec sed -i s/"f_:"/"f_f:"/g {} \;
find . -type f -exec sed -i s/"f_'_"/"f_f'"/g {} \;
find . -type f -exec sed -i s/"eqs_"/"eqs"/g {} \;
find . -type f -exec sed -i s/"f'_ "/"f_f' "/g {} \;
find . -type f -exec sed -i s/"f'_)"/"f_f')"/g {} \;
haftmann@20831
     1
Learning and using Isabelle
wenzelm@18555
     2
  tutorial        Tutorial on Isabelle/HOL
wenzelm@30459
     3
  main            What's in Main
wenzelm@18555
     4
  isar-overview   Tutorial on Isar
wenzelm@18555
     5
  locales         Tutorial on Locales
haftmann@22736
     6
  classes         Tutorial on Type Classes
haftmann@21868
     7
  functions       Tutorial on Function Definitions
haftmann@21868
     8
  codegen         Tutorial on Code Generation
blanchet@36922
     9
  nitpick         User's Guide to Nitpick
blanchet@36922
    10
  sledgehammer    User's Guide to Sledgehammer
wenzelm@30467
    11
  sugar           LaTeX Sugar for Isabelle documents
kleing@14491
    12
kleing@14491
    13
Reference Manuals
wenzelm@18555
    14
  isar-ref        The Isabelle/Isar Reference Manual
haftmann@25244
    15
  implementation  The Isabelle/Isar Implementation Manual
wenzelm@18555
    16
  system          The Isabelle System Manual
wenzelm@30073
    17
wenzelm@30852
    18
Old Manuals (outdated)
wenzelm@30118
    19
  intro           Old Introduction to Isabelle
wenzelm@30118
    20
  ref             Old Isabelle Reference Manual
wenzelm@18555
    21
  logics          Isabelle's Logics: overview and misc logics
wenzelm@18555
    22
  logics-HOL      Isabelle's Logics: HOL
wenzelm@18555
    23
  logics-ZF       Isabelle's Logics: FOL and ZF
wenzelm@30073
    24
  ind-defs        (Co)Inductive Definitions in ZF