FailedChanges

Summary

  1. reverted the substitution here
  2. merged
  3. clarified;
  4. evaluate Scala via running Isabelle/Scala;
  5. more robust: avoid spurious line breaks that might confuse the scala interpreter;
  6. clarified signature: proper eval/print via interpret;
  7. clarified name;
  8. factored out typedef material
  9. tuned;
  10. tuned;
  11. tuned;
  12. proper platform_path for Windows;
  13. evaluate PolyML via running Isabelle/ML;
  14. output via file instead of stdout;
  15. proper context;
  16. clarified signature;
  17. tuned signature;
  18. fixed some remarkably ugly proofs
  19. de-applying and tidying
Changeset 72533:6fdeef6d6335 by paulson _lp15@cam.ac.uk_:
reverted the substitution here
The file was modifiedsrc/HOL/Library/Permutations.thy (diff)
Changeset 72532:4e649ea1f76b by paulson:
merged
Changeset 72531:bc31c4a2c77c by wenzelm:
clarified;
The file was modifiedsrc/HOL/Library/code_test.ML (diff)
Changeset 72530:00490c408e52 by wenzelm:
evaluate Scala via running Isabelle/Scala;
The file was modifiedsrc/HOL/Library/code_test.ML (diff)
Changeset 72529:aafec95bc30e by wenzelm:
more robust: avoid spurious line breaks that might confuse the scala interpreter;
The file was modifiedsrc/Tools/Code/code_scala.ML (diff)
Changeset 72528:25c6423ec538 by wenzelm:
clarified signature: proper eval/print via interpret;
The file was modifiedsrc/Pure/System/scala.scala (diff)
The file was modifiedsrc/Pure/System/scala_compiler.ML (diff)
Changeset 72527:584aea0b29bb by wenzelm:
clarified name;
The file was modifiedsrc/HOL/Library/code_test.ML (diff)
Changeset 72526:4a58c38b85ff by haftmann:
factored out typedef material
The file was modifiedCONTRIBUTORS (diff)
The file was modifiedNEWS (diff)
The file was modifiedsrc/HOL/SPARK/Examples/RIPEMD-160/F.thy (diff)
The file was modifiedsrc/HOL/SPARK/Examples/RIPEMD-160/Round.thy (diff)
The file was modifiedsrc/HOL/Word/Misc_Typedef.thy (diff)
The file was modifiedsrc/HOL/Word/More_Word.thy (diff)
The file was modifiedsrc/HOL/Word/Reversed_Bit_Lists.thy (diff)
The file was modifiedsrc/HOL/Word/Word.thy (diff)
Changeset 72525:ccc104786829 by wenzelm:
tuned;
The file was modifiedsrc/HOL/Library/code_test.ML (diff)
Changeset 72524:811d5eec65a6 by wenzelm:
tuned;
The file was modifiedsrc/HOL/Library/code_test.ML (diff)
Changeset 72523:32d5e474633a by wenzelm:
tuned;
The file was modifiedsrc/HOL/Library/code_test.ML (diff)
Changeset 72522:03628da91b07 by wenzelm:
proper platform_path for Windows;
The file was modifiedsrc/HOL/Library/code_test.ML (diff)
The file was modifiedsrc/Pure/ML/ml_syntax.ML (diff)
Changeset 72521:697e5688f370 by wenzelm:
evaluate PolyML via running Isabelle/ML;
The file was modifiedsrc/HOL/Library/code_test.ML (diff)
Changeset 72520:e4a317d00489 by wenzelm:
output via file instead of stdout;
The file was modifiedsrc/HOL/Library/code_test.ML (diff)
Changeset 72519:989bd067ae30 by wenzelm:
proper context;
The file was modifiedsrc/HOL/Library/code_test.ML (diff)
Changeset 72518:38497ecb4892 by wenzelm:
clarified signature;
The file was modifiedsrc/HOL/Library/code_test.ML (diff)
Changeset 72517:c0d04c740b8a by wenzelm:
tuned signature;
The file was modifiedsrc/HOL/Library/code_test.ML (diff)
Changeset 72516:d7d90ed4c74e by paulson _lp15@cam.ac.uk_:
fixed some remarkably ugly proofs
The file was modifiedsrc/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
The file was modifiedsrc/HOL/Analysis/Polytope.thy (diff)
The file was modifiedsrc/HOL/Analysis/Simplex_Content.thy (diff)
The file was modifiedsrc/HOL/Analysis/Starlike.thy (diff)
The file was modifiedsrc/HOL/Binomial.thy (diff)
The file was modifiedsrc/HOL/Finite_Set.thy (diff)
The file was modifiedsrc/HOL/Library/FSet.thy (diff)
The file was modifiedsrc/HOL/Library/Infinite_Set.thy (diff)
The file was modifiedsrc/HOL/Library/Perm.thy (diff)
The file was modifiedsrc/HOL/Library/Permutations.thy (diff)
The file was modifiedsrc/HOL/List.thy (diff)
The file was modifiedsrc/HOL/Number_Theory/Quadratic_Reciprocity.thy (diff)
The file was modifiedsrc/HOL/SPARK/Examples/Liseq/Longest_Increasing_Subsequence.thy (diff)
The file was modifiedsrc/HOL/Set_Interval.thy (diff)
The file was modifiedsrc/HOL/Vector_Spaces.thy (diff)
Changeset 72515:c5d1a01d2d6c by paulson _lp15@cam.ac.uk_:
de-applying and tidying
The file was modifiedsrc/HOL/Analysis/Complex_Transcendental.thy (diff)