Session HOL-Metis_Examples

Theories

• Abstraction
• HOL-Decision_Procs.Dense_Linear_Order
  • File ‹langford_data.ML›
  • File ‹ferrante_rackoff_data.ML›
  • File ‹langford.ML›
  • File ‹ferrante_rackoff.ML›
• Big_O
• Binary_Tree
• Clausification
• Message
• Type_Encodings
• Proxies
• Sets
• Sledgehammer_Isar_Proofs
  • File ‹Sledgehammer_Isar_Proofs.certs›
• Tarski
• Trans_Closure