Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Changes from Mercurial (hg https://bitbucket.org/isa-afp/afp-devel/ default)

Summary

  1. Fix Lp
  2. Add a theorem by Kohlberg and Neyman on semicontractions
  3. Add a lemma by Benoist-Quint on cohomologous functions
  4. Modernize, simplify, add more text explanations
Changeset 7745:e1df3d2838de by sgouezel:
Fix Lp
The file was modified thys/Lp/Lp.thy
Changeset 7744:4f12bc22a91d by sgouezel:
Add a theorem by Kohlberg and Neyman on semicontractions
The file was addedthys/Ergodic_Theory/Kohlberg_Neyman_Karlsson.thy
The file was modified thys/Ergodic_Theory/ROOT
Changeset 7743:a32e8fd30744 by sgouezel:
Add a lemma by Benoist-Quint on cohomologous functions
The file was modified thys/Ergodic_Theory/Invariants.thy
Changeset 7742:290bd4f1b756 by sgouezel:
Modernize, simplify, add more text explanations
The file was addedthys/Ergodic_Theory/Asymptotic_Density.thy
The file was modified thys/Ergodic_Theory/Ergodicity.thy
The file was modified thys/Ergodic_Theory/Fekete.thy
The file was modified thys/Ergodic_Theory/Gouezel_Karlsson.thy
The file was modified thys/Ergodic_Theory/Invariants.thy
The file was modified thys/Ergodic_Theory/Kingman.thy
The file was modified thys/Ergodic_Theory/Measure_Preserving_Transformations.thy
The file was modified thys/Ergodic_Theory/ROOT
The file was modified thys/Ergodic_Theory/Recurrence.thy
The file was modified thys/Ergodic_Theory/SG_Library_Complement.thy
The file was removedthys/Ergodic_Theory/Banach_Density.thy

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. merged
  2. misc tuning and modernization;
  3. support to encode/decode command state; support to merge full contents of command state;
  4. tuned;
  5. more operations;
  6. tuned signature;
  7. eliminated redundant check (see also 27328dcaf64c vs. 9c53198dbb1c);
  8. Corrected affiliation.
Changeset 65337:27144776aefe by wenzelm:
merged
Changeset 65336:8e5274fc0093 by wenzelm:
misc tuning and modernization;
The file was modified src/HOL/Word/Tools/smt_word.ML
The file was modified src/HOL/Word/Word.thy
Changeset 65335:7634d33c1a79 by wenzelm:
support to encode/decode command state;<br>support to merge full contents of command state;
The file was modified src/Pure/General/symbol.scala
The file was modified src/Pure/Isar/token.scala
The file was modified src/Pure/PIDE/command.scala
The file was modified src/Pure/PIDE/command_span.scala
The file was modified src/Pure/PIDE/markup.scala
Changeset 65334:264a3904ab5a by wenzelm:
tuned;
The file was modified src/Pure/PIDE/xml.scala
Changeset 65333:289561ca4fa3 by wenzelm:
more operations;
The file was modified src/Pure/PIDE/xml.ML
The file was modified src/Pure/PIDE/xml.scala
Changeset 65332:7dbb780f24a9 by wenzelm:
tuned signature;
The file was modified src/Pure/PIDE/document.scala
The file was modified src/Tools/jEdit/src/jedit_rendering.scala
The file was modified src/Tools/jEdit/src/rich_text_area.scala
Changeset 65331:999864cdf96c by wenzelm:
eliminated redundant check (see also 27328dcaf64c vs. 9c53198dbb1c);
The file was modified src/Tools/jEdit/src/document_view.scala
Changeset 65330:d83f709b7580 by ballarin:
Corrected affiliation.
The file was modified CONTRIBUTORS