Session HOL-Induct
View
theory dependencies
View
document
View
outline
Theories
Common_Patterns
Nested_Datatype
QuoDataType
QuoNestedDataType
Term
Sexp
SList
ABexp
Infinitely_Branching_Tree
Ordinals
Sigma_Algebra
Comb
PropLog
Com