Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. updated documentation;
  3. avoid Isabelle symbols in URL;
  4. formal URLs;
  5. tuned spacing;
  6. modernized tags: default scope excludes proof;
  7. report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
  8. support "tag" marker with scope;
  9. tidying up messy proofs about group element order
  10. merged
  11. simpler and stronger proofs
Changeset 70141:5965a0a60c85 by wenzelm:
merged
Changeset 70140:d13865c21e36 by wenzelm:
updated documentation;
The file was modified NEWS (diff)
The file was modified src/Doc/Isar_Ref/Document_Preparation.thy (diff)
Changeset 70139:fd4960dfad2a by wenzelm:
avoid Isabelle symbols in URL;
The file was modified src/HOL/Analysis/Change_Of_Vars.thy (diff)
Changeset 70138:bd42cc1e10d0 by wenzelm:
formal URLs;
The file was modified src/HOL/Analysis/Change_Of_Vars.thy (diff)
The file was modified src/HOL/Analysis/Generalised_Binomial_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
The file was modified src/HOL/Analysis/Weierstrass_Theorems.thy (diff)
Changeset 70137:824c047db30b by wenzelm:
tuned spacing;
The file was modified src/HOL/Analysis/Product_Vector.thy (diff)
Changeset 70136:f03a01a18c6e by wenzelm:
modernized tags: default scope excludes proof;
The file was modified src/HOL/Analysis/Abstract_Topology.thy (diff)
The file was modified src/HOL/Analysis/Abstract_Topology_2.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/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/Bounded_Continuous_Function.thy (diff)
The file was modified src/HOL/Analysis/Bounded_Linear_Function.thy (diff)
The file was modified src/HOL/Analysis/Brouwer_Fixpoint.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/Cauchy_Integral_Theorem.thy (diff)
The file was modified src/HOL/Analysis/Change_Of_Vars.thy (diff)
The file was modified src/HOL/Analysis/Complete_Measure.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/Connected.thy (diff)
The file was modified src/HOL/Analysis/Continuous_Extension.thy (diff)
The file was modified src/HOL/Analysis/Continuum_Not_Denumerable.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/Cross3.thy (diff)
The file was modified src/HOL/Analysis/Derivative.thy (diff)
The file was modified src/HOL/Analysis/Determinants.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/Elementary_Topology.thy (diff)
The file was modified src/HOL/Analysis/Embed_Measure.thy (diff)
The file was modified src/HOL/Analysis/Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Extended_Real_Limits.thy (diff)
The file was modified src/HOL/Analysis/FPS_Convergence.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/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/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/Infinite_Set_Sum.thy (diff)
The file was modified src/HOL/Analysis/Inner_Product.thy (diff)
The file was modified src/HOL/Analysis/Integral_Test.thy (diff)
The file was modified src/HOL/Analysis/Interval_Integral.thy (diff)
The file was modified src/HOL/Analysis/Jordan_Curve.thy (diff)
The file was modified src/HOL/Analysis/L2_Norm.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/Measurable.thy (diff)
The file was modified src/HOL/Analysis/Measure_Space.thy (diff)
The file was modified src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy (diff)
The file was modified src/HOL/Analysis/Norm_Arith.thy (diff)
The file was modified src/HOL/Analysis/Operator_Norm.thy (diff)
The file was modified src/HOL/Analysis/Ordered_Euclidean_Space.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/Product_Vector.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/Set_Integral.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/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/Weierstrass_Theorems.thy (diff)
The file was modified src/HOL/Analysis/Winding_Numbers.thy (diff)
The file was modified src/HOL/Homology/Invariance_of_Domain.thy (diff)
Changeset 70135:ad6d4a14adb5 by wenzelm:
report document tags as seen in the text (not the active tag of Thy_Output.present_thy);
The file was modified src/Pure/PIDE/markup.ML (diff)
The file was modified src/Pure/PIDE/markup.scala (diff)
The file was modified src/Pure/PIDE/rendering.scala (diff)
The file was modified src/Pure/Thy/document_marker.ML (diff)
Changeset 70134:e69f00f4b897 by wenzelm:
support "tag" marker with scope;
The file was modified src/Pure/Isar/outer_syntax.ML (diff)
The file was modified src/Pure/Isar/toplevel.ML (diff)
The file was modified src/Pure/Thy/document_marker.ML (diff)
The file was modified src/Pure/Thy/document_source.ML (diff)
The file was modified src/Pure/Thy/thy_header.ML (diff)
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 70133:4f19b92ab6d7 by paulson _lp15@cam.ac.uk_:
tidying up messy proofs about group element order
The file was modified src/HOL/Algebra/Multiplicative_Group.thy (diff)
Changeset 70132:4ce88d646767 by paulson:
merged
Changeset 70131:c6e1a4806f49 by paulson _lp15@cam.ac.uk_:
simpler and stronger proofs
The file was modified src/HOL/Algebra/Multiplicative_Group.thy (diff)