Session Continued_Fractions
View
theory dependencies
View
document
View
outline
Theories
HOL-Library.Sublist
HOL-Library.Case_Converter
File ‹case_converter.ML›
HOL-Library.Simps_Case_Conv
File ‹simps_case_conv.ML›
HOL-Library.Complete_Partial_Order2
Coinductive.Coinductive_Nat
Coinductive.Coinductive_List
Coinductive.Lazy_LList
HOL-Number_Theory.Fib
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-Library.Stream
HOL-Library.Linear_Temporal_Logic_on_Streams
Coinductive.Coinductive_Stream
Continued_Fractions
HOL-Library.More_List
HOL-Computational_Algebra.Polynomial
HOL-Computational_Algebra.Polynomial_FPS
HOL-Computational_Algebra.Formal_Laurent_Series
HOL-Computational_Algebra.Fraction_Field
HOL-Computational_Algebra.Fundamental_Theorem_Algebra
HOL-Computational_Algebra.Group_Closure
HOL-Computational_Algebra.Normalized_Fraction
HOL-Computational_Algebra.Nth_Powers
HOL-Computational_Algebra.Polynomial_Factorial
HOL-Computational_Algebra.Squarefree
HOL-Computational_Algebra.Computational_Algebra
Quadratic_Irrationals
E_CFrac
HOL-Library.While_Combinator
HOL-Library.IArray
Sqrt_Nat_Cfrac
Pell.Pell
HOL-Library.Tree
Pell.Efficient_Discrete_Sqrt
Pell.Pell_Algorithm
Matrix.Utility
HOL-Library.Adhoc_Overloading
File ‹adhoc_overloading.ML›
HOL-Library.Monad_Syntax
Polynomial_Factorization.Missing_List
Polynomial_Factorization.Missing_Multiset
Polynomial_Factorization.Prime_Factorization
Pell_Lifting
Pell_Continued_Fraction
HOL-Library.Code_Lazy
File ‹code_lazy.ML›
HOL-Library.Code_Target_Int
HOL-Library.Code_Abstract_Nat
HOL-Library.Code_Target_Nat
HOL-Library.Code_Target_Numeral
Pell_Continued_Fraction_Tests
HOL-Library.Lattice_Algebras
HOL-Library.Interval
HOL-Library.Log_Nat
HOL-Library.Float
HOL-Library.Interval_Float
HOL-Decision_Procs.Dense_Linear_Order
File ‹langford_data.ML›
File ‹ferrante_rackoff_data.ML›
File ‹langford.ML›
File ‹ferrante_rackoff.ML›
HOL-Decision_Procs.Approximation_Bounds
HOL-Library.Code_Target_Numeral_Float
HOL-Decision_Procs.Approximation
File ‹approximation.ML›
File ‹approximation_generator.ML›
Continued_Fraction_Approximation
File ‹approximation_cfrac.ML›