Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. reverted the substitution here
  3. merged
  4. fixed some remarkably ugly proofs
  5. de-applying and tidying
  6. follow Phabricator update 2020 Week 37;
  7. clarified defaults for nitpick;
  8. tuned nitpick message: more like quickcheck;
  9. clarified;
  10. evaluate Scala via running Isabelle/Scala;
  11. more robust: avoid spurious line breaks that might confuse the scala interpreter;
  12. clarified signature: proper eval/print via interpret;
  13. clarified name;
  14. factored out typedef material
Changeset 72305:6f0e85e16d84 by paulson:
merged
Changeset 72304:6fdeef6d6335 by paulson _lp15@cam.ac.uk_:
reverted the substitution here
The file was modified src/HOL/Library/Permutations.thy (diff)
Changeset 72303:4e649ea1f76b by paulson:
merged
Changeset 72302:d7d90ed4c74e by paulson _lp15@cam.ac.uk_:
fixed some remarkably ugly proofs
The file was modified src/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
The file was modified src/HOL/Analysis/Polytope.thy (diff)
The file was modified src/HOL/Analysis/Simplex_Content.thy (diff)
The file was modified src/HOL/Analysis/Starlike.thy (diff)
The file was modified src/HOL/Binomial.thy (diff)
The file was modified src/HOL/Finite_Set.thy (diff)
The file was modified src/HOL/Library/FSet.thy (diff)
The file was modified src/HOL/Library/Infinite_Set.thy (diff)
The file was modified src/HOL/Library/Perm.thy (diff)
The file was modified src/HOL/Library/Permutations.thy (diff)
The file was modified src/HOL/List.thy (diff)
The file was modified src/HOL/Number_Theory/Quadratic_Reciprocity.thy (diff)
The file was modified src/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy (diff)
The file was modified src/HOL/Set_Interval.thy (diff)
The file was modified src/HOL/Vector_Spaces.thy (diff)
Changeset 72301:c5d1a01d2d6c by paulson _lp15@cam.ac.uk_:
de-applying and tidying
The file was modified src/HOL/Analysis/Complex_Transcendental.thy (diff)
Changeset 72300:9f07e961a2b0 by wenzelm:
follow Phabricator update 2020 Week 37;
The file was modified etc/options (diff)
Changeset 72299:0c7a74a1c6d9 by wenzelm:
clarified defaults for nitpick;
The file was modified NEWS (diff)
The file was modified src/HOL/Tools/etc/options (diff)
Changeset 72298:a540283d6b58 by wenzelm:
tuned nitpick message: more like quickcheck;
The file was modified src/HOL/Tools/Nitpick/nitpick.ML (diff)
Changeset 72297:bc31c4a2c77c by wenzelm:
clarified;
The file was modified src/HOL/Library/code_test.ML (diff)
Changeset 72296:00490c408e52 by wenzelm:
evaluate Scala via running Isabelle/Scala;
The file was modified src/HOL/Library/code_test.ML (diff)
Changeset 72295:aafec95bc30e by wenzelm:
more robust: avoid spurious line breaks that might confuse the scala interpreter;
The file was modified src/Tools/Code/code_scala.ML (diff)
Changeset 72294:25c6423ec538 by wenzelm:
clarified signature: proper eval/print via interpret;
The file was modified src/Pure/System/scala.scala (diff)
The file was modified src/Pure/System/scala_compiler.ML (diff)
Changeset 72293:584aea0b29bb by wenzelm:
clarified name;
The file was modified src/HOL/Library/code_test.ML (diff)
Changeset 72292:4a58c38b85ff by haftmann:
factored out typedef material
The file was modified CONTRIBUTORS (diff)
The file was modified NEWS (diff)
The file was modified src/HOL/SPARK/Examples/RIPEMD-160/F.thy (diff)
The file was modified src/HOL/SPARK/Examples/RIPEMD-160/Round.thy (diff)
The file was modified src/HOL/Word/Misc_Typedef.thy (diff)
The file was modified src/HOL/Word/More_Word.thy (diff)
The file was modified src/HOL/Word/Reversed_Bit_Lists.thy (diff)
The file was modified src/HOL/Word/Word.thy (diff)