Changes

Summary

updated veriT part of Sledgehammer documentation
added para constrasting 'primrec' and 'fun' -- and removed my middle name
dedicated fact collections for algebraic simplification rules potentially splitting goals

Changeset 70819:ed89f20de7ab by blanchet: updated veriT part of Sledgehammer documentation
The file was modified	`src/Doc/Sledgehammer/document/root.tex` (diff)
Changeset 70818:13d6b561b0ea by blanchet: added para constrasting 'primrec' and 'fun' -- and removed my middle name
The file was modified	`src/Doc/Datatypes/Datatypes.thy` (diff)
The file was modified	`src/Doc/Datatypes/document/root.tex` (diff)
The file was modified	`src/Doc/Nitpick/document/root.tex` (diff)
The file was modified	`src/Doc/Sledgehammer/document/root.tex` (diff)
Changeset 70817:dd675800469d by haftmann: dedicated fact collections for algebraic simplification rules potentially splitting goals
The file was modified	`NEWS` (diff)
The file was modified	`src/HOL/Analysis/Abstract_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Arcwise_Connected.thy` (diff)
The file was modified	`src/HOL/Analysis/Ball_Volume.thy` (diff)
The file was modified	`src/HOL/Analysis/Cartesian_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Cauchy_Integral_Theorem.thy` (diff)
The file was modified	`src/HOL/Analysis/Change_Of_Vars.thy` (diff)
The file was modified	`src/HOL/Analysis/Complex_Analysis_Basics.thy` (diff)
The file was modified	`src/HOL/Analysis/Complex_Transcendental.thy` (diff)
The file was modified	`src/HOL/Analysis/Conformal_Mappings.thy` (diff)
The file was modified	`src/HOL/Analysis/Continuous_Extension.thy` (diff)
The file was modified	`src/HOL/Analysis/Convex.thy` (diff)
The file was modified	`src/HOL/Analysis/Convex_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Derivative.thy` (diff)
The file was modified	`src/HOL/Analysis/Elementary_Metric_Spaces.thy` (diff)
The file was modified	`src/HOL/Analysis/Elementary_Normed_Spaces.thy` (diff)
The file was modified	`src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy` (diff)
The file was modified	`src/HOL/Analysis/FPS_Convergence.thy` (diff)
The file was modified	`src/HOL/Analysis/Function_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Further_Topology.thy` (diff)
The file was modified	`src/HOL/Analysis/Gamma_Function.thy` (diff)
The file was modified	`src/HOL/Analysis/Great_Picard.thy` (diff)
The file was modified	`src/HOL/Analysis/Harmonic_Numbers.thy` (diff)
The file was modified	`src/HOL/Analysis/Henstock_Kurzweil_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Homeomorphism.thy` (diff)
The file was modified	`src/HOL/Analysis/Homotopy.thy` (diff)
The file was modified	`src/HOL/Analysis/Improper_Integral.thy` (diff)
The file was modified	`src/HOL/Analysis/Infinite_Products.thy` (diff)
The file was modified	`src/HOL/Analysis/Lebesgue_Measure.thy` (diff)
The file was modified	`src/HOL/Analysis/Linear_Algebra.thy` (diff)
The file was modified	`src/HOL/Analysis/Lipschitz.thy` (diff)
The file was modified	`src/HOL/Analysis/Path_Connected.thy` (diff)
The file was modified	`src/HOL/Analysis/Polytope.thy` (diff)
The file was modified	`src/HOL/Analysis/Radon_Nikodym.thy` (diff)
The file was modified	`src/HOL/Analysis/Riemann_Mapping.thy` (diff)
The file was modified	`src/HOL/Analysis/Simplex_Content.thy` (diff)
The file was modified	`src/HOL/Analysis/Starlike.thy` (diff)
The file was modified	`src/HOL/Analysis/Summation_Tests.thy` (diff)
The file was modified	`src/HOL/Analysis/Tagged_Division.thy` (diff)
The file was modified	`src/HOL/Analysis/Topology_Euclidean_Space.thy` (diff)
The file was modified	`src/HOL/Analysis/Uniform_Limit.thy` (diff)
The file was modified	`src/HOL/Analysis/Vitali_Covering_Theorem.thy` (diff)
The file was modified	`src/HOL/Analysis/Weierstrass_Theorems.thy` (diff)
The file was modified	`src/HOL/Analysis/Winding_Numbers.thy` (diff)
The file was modified	`src/HOL/Analysis/ex/Approximations.thy` (diff)
The file was modified	`src/HOL/Complex.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Computational_Algebra.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Field_as_Ring.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Formal_Laurent_Series.thy` (diff)
The file was modified	`src/HOL/Computational_Algebra/Formal_Power_Series.thy` (diff)
The file was modified	`src/HOL/Decision_Procs/Approximation_Bounds.thy` (diff)
The file was modified	`src/HOL/Fields.thy` (diff)
The file was modified	`src/HOL/Groups.thy` (diff)
The file was modified	`src/HOL/Homology/Simplices.thy` (diff)
The file was modified	`src/HOL/Library/Float.thy` (diff)
The file was modified	`src/HOL/Library/Landau_Symbols.thy` (diff)
The file was modified	`src/HOL/Library/Nonpos_Ints.thy` (diff)
The file was modified	`src/HOL/Limits.thy` (diff)
The file was modified	`src/HOL/MacLaurin.thy` (diff)
The file was modified	`src/HOL/Modules.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Fib.thy` (diff)
The file was modified	`src/HOL/Power.thy` (diff)
The file was modified	`src/HOL/Probability/Conditional_Expectation.thy` (diff)
The file was modified	`src/HOL/Probability/Distributions.thy` (diff)
The file was modified	`src/HOL/Probability/Levy.thy` (diff)
The file was modified	`src/HOL/Probability/Probability_Mass_Function.thy` (diff)
The file was modified	`src/HOL/Probability/Random_Permutations.thy` (diff)
The file was modified	`src/HOL/Real.thy` (diff)
The file was modified	`src/HOL/Real_Asymp/Multiseries_Expansion.thy` (diff)
The file was modified	`src/HOL/Real_Asymp/Multiseries_Expansion_Bounds.thy` (diff)
The file was modified	`src/HOL/Real_Asymp/Real_Asymp_Examples.thy` (diff)
The file was modified	`src/HOL/Real_Vector_Spaces.thy` (diff)
The file was modified	`src/HOL/Rings.thy` (diff)
The file was modified	`src/HOL/Set_Interval.thy` (diff)
The file was modified	`src/HOL/Transcendental.thy` (diff)