HOL-Induct

Common_Patterns

Nested_Datatype

QuoDataType

QuoNestedDataType

Term

Sexp

SList

ABexp

Infinitely_Branching_Tree

Ordinals

Sigma_Algebra

Comb

PropLog

Com