Session ZF

Theories

• ZF_Base
• upair
  • File ‹Tools/typechk.ML›
• pair
  • File ‹simpdata.ML›
• equalities
• Fixedpt
• Bool
• Sum
• func
• QPair
• Perm
• Trancl
• WF
• Ordinal
• OrdQuant
• Nat
• Inductive
  • File ‹ind_syntax.ML›
  • File ‹Tools/ind_cases.ML›
  • File ‹Tools/cartprod.ML›
  • File ‹Tools/inductive_package.ML›
  • File ‹Tools/induct_tacs.ML›
  • File ‹Tools/primrec_package.ML›
• Epsilon
• Order
• OrderArith
• OrderType
• Finite
• Cardinal
• Univ
• QUniv
• Datatype
  • File ‹Tools/datatype_package.ML›
• Arith
• ArithSimp
  • File ‹~~/src/Provers/Arith/cancel_numerals.ML›
  • File ‹~~/src/Provers/Arith/combine_numerals.ML›
  • File ‹arith_data.ML›
• List
• EquivClass
• Int
• Bin
  • File ‹Tools/numeral_syntax.ML›
  • File ‹int_arith.ML›
• IntDiv
• CardinalArith
• ZF
• AC
• Zorn
• Cardinal_AC
• InfDatatype
• ZFC