Session Roth_Arithmetic_Progressions

Theories

• Girth_Chromatic.Girth_Chromatic_Misc
• Girth_Chromatic.Ugraphs
• Szemeredi_Regularity.Szemeredi
• 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_Int
• HOL-Library.Code_Abstract_Nat
• HOL-Library.Code_Target_Nat
• HOL-Library.Code_Target_Numeral
• HOL-Library.Code_Target_Numeral_Float
• HOL-Decision_Procs.Approximation
  • File ‹approximation.ML›
  • File ‹approximation_generator.ML›
• Girth_Chromatic.Girth_Chromatic
• Random_Graph_Subgraph_Threshold.Ugraph_Misc
• Random_Graph_Subgraph_Threshold.Prob_Lemmas
• Random_Graph_Subgraph_Threshold.Ugraph_Lemmas
• Random_Graph_Subgraph_Threshold.Ugraph_Properties
• Random_Graph_Subgraph_Threshold.Subgraph_Threshold
• Ergodic_Theory.SG_Library_Complement
• Ergodic_Theory.Asymptotic_Density
• HOL-Library.Ramsey
• Roth_Arithmetic_Progressions