Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. NEWS: Removed constant subseq; subsumed by strict_mono
  2. support for incremental update according to session graph structure;
  3. Merged
  4. Replaced subseq with strict_mono
  5. fix document
  6. more complete session (amending e77ea0ea7f2c);
  7. clarified imports;
  8. more complete session (amending 783861a66a60);
  9. added lemma
Changeset 66450:a8299195ed82 by eberlm _eberlm@in.tum.de_:
NEWS: Removed constant subseq; subsumed by strict_mono
The file was modified NEWS (diff)
Changeset 66449:1be102db1598 by wenzelm:
support for incremental update according to session graph structure;
The file was modified NEWS (diff)
The file was modified src/Pure/Tools/imports.scala (diff)
Changeset 66448:97ad7a583457 by eberlm _eberlm@in.tum.de_:
Merged
Changeset 66447:a1f5c5c26fa6 by eberlm _eberlm@in.tum.de_:
Replaced subseq with strict_mono
The file was modified src/HOL/Analysis/Bochner_Integration.thy (diff)
The file was modified src/HOL/Analysis/Bounded_Linear_Function.thy (diff)
The file was modified src/HOL/Analysis/Cartesian_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Complex_Transcendental.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/Linear_Algebra.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Set_Integral.thy (diff)
The file was modified src/HOL/Analysis/Summation_Tests.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
The file was modified src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy (diff)
The file was modified src/HOL/Library/Diagonal_Subsequence.thy (diff)
The file was modified src/HOL/Library/Liminf_Limsup.thy (diff)
The file was modified src/HOL/Limits.thy (diff)
The file was modified src/HOL/Probability/Helly_Selection.thy (diff)
The file was modified src/HOL/Probability/Levy.thy (diff)
The file was modified src/HOL/Probability/Projective_Limit.thy (diff)
The file was modified src/HOL/Series.thy (diff)
The file was modified src/HOL/Topological_Spaces.thy (diff)
Changeset 66446:aeb8b8fe94d0 by lars hupel _lars.hupel@mytum.de_:
fix document
The file was modified src/HOL/Word/WordBitwise.thy (diff)
Changeset 66445:407de0768126 by wenzelm:
more complete session (amending e77ea0ea7f2c);
The file was modified src/HOL/ROOT (diff)
Changeset 66444:6d2d993fa76e by wenzelm:
clarified imports;
The file was modified src/CCL/ROOT (diff)
The file was modified src/Doc/ROOT (diff)
The file was modified src/HOL/ROOT (diff)
The file was modified src/LCF/ROOT (diff)
The file was modified src/ZF/ROOT (diff)
Changeset 66443:657c517c7dc6 by wenzelm:
more complete session (amending 783861a66a60);
The file was modified src/HOL/ROOT (diff)
Changeset 66442:050bc74d55ed by nipkow:
added lemma
The file was modified src/HOL/List.thy (diff)