Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. amending 689997a8a582
  2. subsection is always %important
  3. no need for %unimportant for proofs of proposition
  4. redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
  5. revert to 56acd449da41
  6. merge
  7. more tagging
  8. updated tagging for 9 theories: Cross3, Determinants, Tagged_Division, Change_of_Vars, Extended_Real_Limits, Fashoda, Finite_Cartesian_Product, Function_Topology, Finite_Product_Measure
  9. chapters for analysis manual
Changeset 69684:94284d4dab98 by immler:
amending 689997a8a582
The file was modified src/HOL/Analysis/Finite_Cartesian_Product.thy (diff)
Changeset 69683:8b3458ca0762 by immler:
subsection is always %important
The file was modified src/HOL/Analysis/Arcwise_Connected.thy (diff)
The file was modified src/HOL/Analysis/Binary_Product_Measure.thy (diff)
The file was modified src/HOL/Analysis/Bochner_Integration.thy (diff)
The file was modified src/HOL/Analysis/Borel_Space.thy (diff)
The file was modified src/HOL/Analysis/Caratheodory.thy (diff)
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Cartesian_Space.thy (diff)
The file was modified src/HOL/Analysis/Change_Of_Vars.thy (diff)
The file was modified src/HOL/Analysis/Cross3.thy (diff)
The file was modified src/HOL/Analysis/Determinants.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Topology.thy (diff)
The file was modified src/HOL/Analysis/Extended_Real_Limits.thy (diff)
The file was modified src/HOL/Analysis/Fashoda_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Finite_Cartesian_Product.thy (diff)
The file was modified src/HOL/Analysis/Finite_Product_Measure.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/Great_Picard.thy (diff)
The file was modified src/HOL/Analysis/Homeomorphism.thy (diff)
The file was modified src/HOL/Analysis/Improper_Integral.thy (diff)
The file was modified src/HOL/Analysis/Interval_Integral.thy (diff)
The file was modified src/HOL/Analysis/Linear_Algebra.thy (diff)
The file was modified src/HOL/Analysis/Ordered_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Poly_Roots.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/Tagged_Division.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)
Changeset 69682:500a7acdccd4 by immler:
no need for %unimportant for proofs of proposition
The file was modified src/HOL/Analysis/Cross3.thy (diff)
Changeset 69681:689997a8a582 by immler:
redo tagging-related changes from a06b204527e6, 0f4d4a13dc16, and a8faf6f15da7
The file was modified src/HOL/Analysis/Cross3.thy (diff)
The file was modified src/HOL/Analysis/Extended_Real_Limits.thy (diff)
The file was modified src/HOL/Analysis/Fashoda_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Finite_Cartesian_Product.thy (diff)
The file was modified src/HOL/Analysis/Finite_Product_Measure.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/Great_Picard.thy (diff)
The file was modified src/HOL/Analysis/Homeomorphism.thy (diff)
The file was modified src/HOL/Analysis/Improper_Integral.thy (diff)
The file was modified src/HOL/Analysis/Interval_Integral.thy (diff)
The file was modified src/HOL/Analysis/Tagged_Division.thy (diff)
Changeset 69680:96a43caa4902 by immler:
revert to 56acd449da41
The file was modified src/HOL/Analysis/Cross3.thy (diff)
The file was modified src/HOL/Analysis/Determinants.thy (diff)
The file was modified src/HOL/Analysis/Extended_Real_Limits.thy (diff)
The file was modified src/HOL/Analysis/Fashoda_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Finite_Cartesian_Product.thy (diff)
The file was modified src/HOL/Analysis/Finite_Product_Measure.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/Great_Picard.thy (diff)
The file was modified src/HOL/Analysis/Homeomorphism.thy (diff)
The file was modified src/HOL/Analysis/Improper_Integral.thy (diff)
The file was modified src/HOL/Analysis/Interval_Integral.thy (diff)
The file was modified src/HOL/Analysis/Tagged_Division.thy (diff)
Changeset 69679:a8faf6f15da7 by angeliki koutsoukouargyraki _ak2110@cam.ac.uk_:
merge
Changeset 69678:0f4d4a13dc16 by angeliki koutsoukouargyraki _ak2110@cam.ac.uk_:
more tagging
Changeset 69677:a06b204527e6 by angeliki koutsoukouargyraki _ak2110@cam.ac.uk_:
updated tagging for 9 theories: Cross3, Determinants, Tagged_Division, Change_of_Vars, Extended_Real_Limits, Fashoda, Finite_Cartesian_Product, Function_Topology, Finite_Product_Measure
The file was modified NEWS (diff)
The file was modified src/Doc/System/Sessions.thy (diff)
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Cartesian_Space.thy (diff)
The file was modified src/HOL/Analysis/Change_Of_Vars.thy (diff)
The file was modified src/HOL/Analysis/Cross3.thy (diff)
The file was modified src/HOL/Analysis/Determinants.thy (diff)
The file was modified src/HOL/Analysis/Extended_Real_Limits.thy (diff)
The file was modified src/HOL/Analysis/Fashoda_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Finite_Cartesian_Product.thy (diff)
The file was modified src/HOL/Analysis/Finite_Product_Measure.thy (diff)
The file was modified src/HOL/Analysis/Function_Topology.thy (diff)
The file was modified src/HOL/Analysis/Henstock_Kurzweil_Integration.thy (diff)
The file was modified src/HOL/Analysis/Tagged_Division.thy (diff)
The file was modified src/HOL/Library/Cardinality.thy (diff)
The file was modified src/HOL/Library/Numeral_Type.thy (diff)
The file was modified src/Pure/General/path.ML (diff)
The file was modified src/Pure/General/path.scala (diff)
The file was modified src/Pure/Pure.thy (diff)
The file was modified src/Pure/Thy/export.scala (diff)
The file was modified src/Pure/Thy/sessions.ML (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/Tools/generated_files.ML (diff)
The file was modified src/Tools/Haskell/Haskell.thy (diff)
The file was modified src/Tools/Haskell/Test.thy (diff)
Changeset 69676:56acd449da41 by immler:
chapters for analysis manual
The file was modified src/HOL/Analysis/Analysis.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Metric_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Elementary_Topology.thy (diff)
The file was modified src/HOL/Analysis/L2_Norm.thy (diff)
The file was modified src/HOL/Analysis/Sigma_Algebra.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/document/root.tex (diff)