Session LCF

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›
• LCF
• Ex1
• Ex2
• Ex3
• Ex4