Session HOL-Examples

Theories

• HOL-Library.Infinite_Set
• HOL-Library.Adhoc_Overloading
  • File ‹adhoc_overloading.ML›
• Adhoc_Overloading_Examples
• 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-Library.Multiset_Order
• HOL-Library.Product_Lexorder
• Ackermann
• Cantor
• Coherent
• Commands
• Drinker
• HOL-Library.Monad_Syntax
• Functions
• HOL-Library.Centered_Division
• Gauss_Numbers
• Groebner_Examples
• Iff_Oracle
• Induction_Schema
• Knaster_Tarski
• ML
• Peirce
• Records
• HOL-Library.Rewrite
  • File ‹cconv.ML›
  • File ‹rewrite.ML›
• Rewrite_Examples
• Seq
• HOL-Computational_Algebra.Factorial_Ring
• HOL-Computational_Algebra.Euclidean_Algorithm
• HOL-Computational_Algebra.Primes
• Sqrt