Session HOL-Proofs-Extraction

Theories

• Util
• QuotRem
• Greatest_Common_Divisor
• Warshall
• Higman
• HOL-Library.Open_State_Syntax
• Higman_Extraction
• HOL-Library.Code_Target_Int
• HOL-Library.Code_Abstract_Nat
• HOL-Library.Code_Target_Nat
• HOL-Library.Code_Target_Numeral
• Pigeonhole
• HOL-Library.Cancellation
  • File ‹Cancellation/cancel.ML›
  • File ‹Cancellation/cancel_data.ML›
  • File ‹Cancellation/cancel_simprocs.ML›
• HOL-Library.Multiset
  • File ‹multiset_simprocs.ML›
• HOL-Computational_Algebra.Factorial_Ring
• HOL-Computational_Algebra.Euclidean_Algorithm
• HOL-Computational_Algebra.Primes
• Euclid