Session ZF

Theories

• IFOL
  • File ‹~~/src/Tools/misc_legacy.ML›
  • File ‹~~/src/Provers/splitter.ML›
  • File ‹~~/src/Provers/hypsubst.ML›
  • File ‹~~/src/Tools/IsaPlanner/zipper.ML›
  • File ‹~~/src/Tools/IsaPlanner/isand.ML›
  • File ‹~~/src/Tools/IsaPlanner/rw_inst.ML›
  • File ‹~~/src/Provers/quantifier1.ML›
  • File ‹~~/src/Tools/intuitionistic.ML›
  • File ‹~~/src/Tools/project_rule.ML›
  • File ‹~~/src/Tools/atomize_elim.ML›
  • File ‹fologic.ML›
  • File ‹intprover.ML›
• FOL
  • File ‹~~/src/Provers/classical.ML›
  • File ‹~~/src/Provers/blast.ML›
  • File ‹~~/src/Provers/clasimp.ML›
  • File ‹simpdata.ML›
  • File ‹~~/src/Tools/eqsubst.ML›
  • File ‹~~/src/Tools/induct.ML›
  • File ‹~~/src/Tools/case_product.ML›
• 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