Changes

Summary

More binomial material
syntax of gchoose now the same as choose
Some new simprules – and patches for proofs
merged
merged
A little more tidying in Nominal

Changeset 80177:1478555580af by paulson _lp15@cam.ac.uk_: More binomial material
The file was added	`src/HOL/Binomial_Plus.thy`
The file was modified	`src/HOL/Complex_Main.thy` (diff)
The file was modified	`src/HOL/Transcendental.thy` (diff)
Changeset 80176:7fefa7839ac6 by paulson _lp15@cam.ac.uk_: syntax of gchoose now the same as choose
The file was modified	`src/HOL/Binomial.thy` (diff)
Changeset 80175:200107cdd3ac by paulson _lp15@cam.ac.uk_: Some new simprules – and patches for proofs
The file was modified	`src/HOL/Analysis/Arcwise_Connected.thy` (diff)
The file was modified	`src/HOL/Analysis/Bochner_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Further_Topology.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/Kronecker_Approximation_Theorem.thy` (diff)
The file was modified	`src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy` (diff)
The file was modified	`src/HOL/Analysis/Starlike.thy` (diff)
The file was modified	`src/HOL/Analysis/Weierstrass_Theorems.thy` (diff)
The file was modified	`src/HOL/Binomial.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/Filter.thy` (diff)
The file was modified	`src/HOL/HOLCF/Universal.thy` (diff)
The file was modified	`src/HOL/Homology/Homology_Groups.thy` (diff)
The file was modified	`src/HOL/Lattices_Big.thy` (diff)
The file was modified	`src/HOL/Library/Landau_Symbols.thy` (diff)
The file was modified	`src/HOL/Nat.thy` (diff)
The file was modified	`src/HOL/NthRoot.thy` (diff)
The file was modified	`src/HOL/Number_Theory/Quadratic_Reciprocity.thy` (diff)
The file was modified	`src/HOL/Probability/Sinc_Integral.thy` (diff)
The file was modified	`src/HOL/Random.thy` (diff)
The file was modified	`src/HOL/Real_Asymp/Multiseries_Expansion.thy` (diff)
The file was modified	`src/HOL/Transcendental.thy` (diff)
The file was modified	`src/HOL/ex/HarmonicSeries.thy` (diff)
Changeset 80174:32d2b96affc7 by paulson: merged
Changeset 80173:8e486ad63579 by paulson: merged
Changeset 80172:6c62605cb3f6 by paulson _lp15@cam.ac.uk_: A little more tidying in Nominal
The file was modified	`src/HOL/Nominal/Examples/Class1.thy` (diff)