Session ZFC_in_HOL

Theories

• 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.Infinite_Set
• HOL-Library.Countable_Set
• HOL-Library.FuncSet
• HOL-Library.Equipollence
• HOL-Cardinals.Fun_More
• HOL-Cardinals.Order_Relation_More
• HOL-Cardinals.Wellfounded_More
• HOL-Cardinals.Wellorder_Relation
• HOL-Cardinals.Wellorder_Embedding
• HOL-Cardinals.Order_Union
• HOL-Cardinals.Wellorder_Constructions
• HOL-Cardinals.Ordinal_Arithmetic
• HOL-Cardinals.Cardinal_Order_Relation
• HOL-Cardinals.Cardinal_Arithmetic
• HOL-Cardinals.Wellorder_Extension
• HOL-Cardinals.Cardinals
• ZFC_Library
• ZFC_in_HOL
• ZFC_Cardinals
• Kirby
• Ordinal_Exp
• Cantor_NF
• ZFC_Typeclasses
• HOL-Analysis.Continuum_Not_Denumerable
• General_Cardinals