Session Linear_Recurrences
View
theory dependencies
View
document
View
outline
Theories
HOL-Computational_Algebra.Group_Closure
HOL-Computational_Algebra.Nth_Powers
HOL-Computational_Algebra.Squarefree
HOL-Computational_Algebra.Computational_Algebra
RatFPS
HOL-Combinatorics.Stirling
Pochhammer_Polynomials
HOL-Library.Sublist
Linear_Recurrences_Misc
Partial_Fraction_Decomposition
Factorizations
Rational_FPS_Solver
Linear_Recurrences_Common
Linear_Homogenous_Recurrences
Eulerian_Polynomials
Linear_Inhomogenous_Recurrences
Matrix.Utility
Polynomial_Factorization.Polynomial_Divisibility
Polynomial_Factorization.Order_Polynomial
Polynomial_Factorization.Fundamental_Theorem_Algebra_Factorized
Polynomial_Factorization.Square_Free_Factorization
HOL-Library.BNF_Corec
File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_tactics.ML›
File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec.ML›
File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_util.ML›
File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar_tactics.ML›
File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML›
File ‹~~/src/HOL/Tools/BNF/bnf_gfp_grec_unique_sugar.ML›
HOL-Real_Asymp.Lazy_Eval
File ‹lazy_eval.ML›
HOL-Real_Asymp.Inst_Existentials
File ‹inst_existentials.ML›
HOL-Real_Asymp.Eventuallize
HOL-Real_Asymp.Multiseries_Expansion
File ‹asymptotic_basis.ML›
File ‹exp_log_expression.ML›
File ‹expansion_interface.ML›
File ‹multiseries_expansion.ML›
File ‹real_asymp.ML›
HOL-Real_Asymp.Multiseries_Expansion_Bounds
File ‹multiseries_expansion_bounds.ML›
HOL-Real_Asymp.Real_Asymp
File ‹real_asymp_diag.ML›
HOL-Library.Code_Target_Int
HOL-Library.Code_Abstract_Nat
HOL-Library.Code_Target_Nat
HOL-Library.Code_Target_Numeral
Rational_FPS_Asymptotics