author desharna
Mon, 20 Mar 2023 18:33:56 +0100
changeset 77699 d5060a919b3f
parent 76479 8ac1d83301b5
permissions -rw-r--r--
reordered assumption and tuned proof of Multiset.bex_least_element and Multiset.bex_greatest_element

Isabelle Tutorials!
  prog-prove      Programming and Proving in Isabelle/HOL
  locales         Tutorial on Locales
  classes         Tutorial on Type Classes
  datatypes       Tutorial on (Co)datatype Definitions
  functions       Tutorial on Function Definitions
  corec           Tutorial on Nonprimitively Corecursive Definitions
  codegen         Tutorial on Code Generation
  nitpick         User's Guide to Nitpick
  sledgehammer    User's Guide to Sledgehammer
  eisbach         The Eisbach User Manual
  sugar           LaTeX Sugar for Isabelle documents

Isabelle Reference Manuals!
  main            What's in Main
  isar-ref        The Isabelle/Isar Reference Manual
  implementation  The Isabelle/Isar Implementation Manual
  system          The Isabelle System Manual
  jedit           Isabelle/jEdit

Demo Documents
  demo_easychair  Demo for Easychair LaTeX style
  demo_eptcs      Demo for EPTCS LaTeX style
  demo_foiltex    Demo for FoilTeX: slides in LaTeX
  demo_lipics     Demo for Dagstuhl LIPIcs style
  demo_llncs      Demo for Springer LaTeX LNCS style

Old Isabelle Manuals
  tutorial        Tutorial on Isabelle/HOL
  intro           Old Introduction to Isabelle
  logics          Isabelle's Logics: HOL and misc logics
  logics-ZF       Isabelle's Logics: FOL and ZF