Session HOL-Induct

Theories

• Common_Patterns
• Nested_Datatype
• QuoDataType
• QuoNestedDataType
• Term
• HOL-Library.Old_Datatype
  • File ‹~~/src/HOL/Tools/Old_Datatype/old_datatype.ML›
• Sexp
• SList
• ABexp
• Infinitely_Branching_Tree
• Ordinals
• Sigma_Algebra
• Comb
• PropLog
• Com