Session CCL

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›
• Set
• Lfp
• Gfp
• CCL
• Trancl
• Term
• Type
• Hered
• Wfd
• Fix
• Nat
• List
• Stream
• Flag