Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned;
  2. tuned;
  3. merge plus tidied three proofs
  4. merged
  5. merged
  6. type instantiations for poly_mapping as a real_normed_vector
  7. visible hairline for cursor, even on OpenJDK 11 (amending 2fd73a1a0937);
  8. tuned signature according to ML version;
  9. strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
  10. added document antiquotation option "cartouche";
  11. allow faster navigation of directory hierarchy (reverting 69465c3e3560);
  12. more robust test: avoid spurious Interrupt (stack overflow?) due to List.fun_lub_parametric;
  13. prefer local options;
  14. tuned signature; tuned message;
  15. clarified order;
  16. merged
  17. prod/sum fixes
  18. Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context
Changeset 70130:c7866e763e9f by wenzelm:
tuned;
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 70129:740db500654d by wenzelm:
tuned;
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 70128:f2f797260010 by paulson _lp15@cam.ac.uk_:
merge plus tidied three proofs
The file was modified src/HOL/Groups_Big.thy (diff)
Changeset 70127:538d9854ca2f by paulson:
merged
Changeset 70126:e0ac5e71a964 by paulson:
merged
Changeset 70125:b601c2c87076 by paulson _lp15@cam.ac.uk_:
type instantiations for poly_mapping as a real_normed_vector
The file was addedsrc/HOL/Analysis/Finite_Function_Topology.thy
The file was modified NEWS (diff)
The file was modified src/HOL/Homology/Invariance_of_Domain.thy (diff)
The file was modified src/HOL/Probability/Conditional_Expectation.thy (diff)
Changeset 70124:af4f723823d8 by wenzelm:
visible hairline for cursor, even on OpenJDK 11 (amending 2fd73a1a0937);
The file was modified src/Tools/jEdit/src/syntax_style.scala (diff)
Changeset 70123:b256f67e9d27 by wenzelm:
tuned signature according to ML version;
The file was modified src/Pure/Isar/keyword.scala (diff)
Changeset 70122:a0b21b4b7a4a by wenzelm:
strip cartouches from arguments of "embedded" document antiquotations, corresponding to automated update via "isabelle update -u control_cartouches" -- e.g. relevant for documents with thy_output_source (e.g. doc "isar-ref", "jedit", "system");
The file was modified NEWS (diff)
The file was modified etc/options (diff)
The file was modified src/Doc/Isar_Ref/Document_Preparation.thy (diff)
The file was modified src/Pure/Thy/document_antiquotation.ML (diff)
The file was modified src/Pure/Thy/document_antiquotations.ML (diff)
The file was modified src/Pure/Thy/thy_output.ML (diff)
Changeset 70121:61e26527480e by wenzelm:
added document antiquotation option "cartouche";
The file was modified NEWS (diff)
The file was modified etc/options (diff)
The file was modified src/Doc/Isar_Ref/Document_Preparation.thy (diff)
The file was modified src/Doc/antiquote_setup.ML (diff)
The file was modified src/Pure/Thy/document_antiquotation.ML (diff)
Changeset 70120:45ca4006a37f by wenzelm:
allow faster navigation of directory hierarchy (reverting 69465c3e3560);
The file was modified src/Tools/jEdit/src/jEdit.props (diff)
Changeset 70119:b48a496ca0cd by wenzelm:
more robust test: avoid spurious Interrupt (stack overflow?) due to List.fun_lub_parametric;
The file was modified src/Benchmarks/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy (diff)
Changeset 70118:62b875ba33e1 by wenzelm:
prefer local options;
The file was modified src/Benchmarks/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy (diff)
Changeset 70117:5ae2f266885f by wenzelm:
tuned signature;<br>tuned message;
The file was modified src/HOL/Tools/Quickcheck/find_unused_assms.ML (diff)
Changeset 70116:3d580b5c4aee by wenzelm:
clarified order;
The file was modified src/HOL/Tools/Quickcheck/find_unused_assms.ML (diff)
Changeset 70115:c59af027a2e5 by paulson:
merged
Changeset 70114:089c17514794 by paulson _lp15@cam.ac.uk_:
prod/sum fixes
The file was modified src/HOL/Analysis/ex/Approximations.thy (diff)
The file was modified src/HOL/Homology/Invariance_of_Domain.thy (diff)
The file was modified src/HOL/ex/Sum_of_Powers.thy (diff)
Changeset 70113:c8deb8ba6d05 by paulson _lp15@cam.ac.uk_:
Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Conformal_Mappings.thy (diff)
The file was modified src/HOL/Analysis/FPS_Convergence.thy (diff)
The file was modified src/HOL/Analysis/Gamma_Function.thy (diff)
The file was modified src/HOL/Analysis/Harmonic_Numbers.thy (diff)
The file was modified src/HOL/Analysis/Infinite_Products.thy (diff)
The file was modified src/HOL/Analysis/Poly_Roots.thy (diff)
The file was modified src/HOL/Analysis/Summation_Tests.thy (diff)
The file was modified src/HOL/Analysis/ex/Approximations.thy (diff)
The file was modified src/HOL/Binomial.thy (diff)
The file was modified src/HOL/Computational_Algebra/Formal_Power_Series.thy (diff)
The file was modified src/HOL/Computational_Algebra/Polynomial.thy (diff)
The file was modified src/HOL/Decision_Procs/Approximation.thy (diff)
The file was modified src/HOL/Factorial.thy (diff)
The file was modified src/HOL/Homology/Homology.thy (diff)
The file was modified src/HOL/Homology/Invariance_of_Domain.thy (diff)
The file was modified src/HOL/Homology/Simplices.thy (diff)
The file was modified src/HOL/Library/Stirling.thy (diff)
The file was modified src/HOL/Library/Uprod.thy (diff)
The file was modified src/HOL/Nonstandard_Analysis/HSeries.thy (diff)
The file was modified src/HOL/Real_Asymp/Multiseries_Expansion.thy (diff)
The file was modified src/HOL/Series.thy (diff)
The file was modified src/HOL/Set_Interval.thy (diff)
The file was modified src/HOL/Transcendental.thy (diff)
The file was modified src/HOL/ex/HarmonicSeries.thy (diff)
The file was modified src/HOL/ex/ThreeDivides.thy (diff)