Session HOL-Computational_Algebra

Theories

• HOL-Library.Cancellation
  • File ‹Cancellation/cancel.ML›
  • File ‹Cancellation/cancel_data.ML›
  • File ‹Cancellation/cancel_simprocs.ML›
• HOL-Library.Multiset
  • File ‹multiset_simprocs.ML›
• Factorial_Ring
• Euclidean_Algorithm
• HOL-Library.More_List
• HOL-Library.Infinite_Set
• Primes
• Polynomial
• HOL-Library.FuncSet
• Formal_Power_Series
• Polynomial_FPS
• Formal_Laurent_Series
• Fraction_Field
• Fundamental_Theorem_Algebra
• Group_Closure
• Normalized_Fraction
• Nth_Powers
• Polynomial_Factorial
• Squarefree
• Computational_Algebra
• Field_as_Ring
• HOL-Library.Discrete_Functions
• HOL-Library.Code_Abstract_Nat
• HOL-Library.Code_Target_Nat
• HOL-Library.Code_Target_Int
• HOL-Library.Code_Target_Numeral
• Computation_Checks