Session BNF_CC
View
theory dependencies
View
document
View
outline
Theories
Preliminaries
HOL-Library.Rewrite
File ‹cconv.ML›
File ‹rewrite.ML›
Axiomatised_BNF_CC
Composition
Fixpoints
HOL-Library.BNF_Axiomatization
File ‹~~/src/HOL/Tools/BNF/bnf_axiomatization.ML›
Subtypes
Quotient_Preservation
Operation_Examples
HOL-Library.Phantom_Type
HOL-Library.Cardinality
Concrete_Examples
HOL-Library.Old_Datatype
File ‹~~/src/HOL/Tools/Old_Datatype/old_datatype.ML›
HOL-Library.Nat_Bijection
HOL-Library.Countable
File ‹~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML›
HOL-Library.FSet
DDS