Session HOL-Eisbach

Theories

• Eisbach
  • File ‹parse_tools.ML›
  • File ‹method_closure.ML›
  • File ‹eisbach_rule_insts.ML›
  • File ‹match_method.ML›
• Eisbach_Tools
• Tests
• Examples
• 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›
• Eisbach_Old_Appl_Syntax
• Examples_FOL
• HOL-Analysis.Metric_Arith
  • File ‹metric_arith.ML›
• Example_Metric