Session Isar_Ref

Theories

• Base
  • File ‹~~/src/Doc/antiquote_setup.ML›
• Preface
• Synopsis
• Framework
• First_Order_Logic
• Outer_Syntax
• Document_Preparation
• Spec
• Proof
• Proof_Script
• Inner_Syntax
• Generic
• HOL-Library.Old_Datatype
  • File ‹~~/src/HOL/Tools/Old_Datatype/old_datatype.ML›
• HOL-Library.Old_Recdef
  • File ‹old_recdef.ML›
• HOL-Library.Adhoc_Overloading
  • File ‹adhoc_overloading.ML›
• HOL-Library.Confluence
• HOL-Library.Confluent_Quotient
• HOL-Library.Dlist
• HOL-Library.Nat_Bijection
• HOL-Library.Countable
  • File ‹~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML›
• HOL-Library.FSet
• HOL_Specific
• Quick_Reference
• Symbols
  • File ‹~~/lib/texinputs/isabellesym.sty›