Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. avoid Scala if-expressions and thus make it work both for -new-syntax or -old-syntax;
  2. proper Scala code for String.literal_of_asciis: avoid ambiguity of ("" ++ ...);
  3. adjust generated Scala to make it work with scalac -old-syntax and -new-syntax, although the latter is not regularly tested;
  4. Add entry on Sketch_and_Explore to CONTRIBUTORS
Changeset 80088:5afbf04418ec by wenzelm:
avoid Scala if-expressions and thus make it work both for -new-syntax or -old-syntax;
The file was modified Admin/Release/CHECKLIST (diff)
The file was modified NEWS (diff)
The file was modified src/HOL/Code_Numeral.thy (diff)
The file was modified src/HOL/HOL.thy (diff)
The file was modified src/HOL/Library/Code_Lazy.thy (diff)
The file was modified src/HOL/String.thy (diff)
Changeset 80087:bda75c790bfa by wenzelm:
proper Scala code for String.literal_of_asciis: avoid ambiguity of ("" ++ ...);
The file was modified src/HOL/String.thy (diff)
Changeset 80086:1b986e5f9764 by wenzelm:
adjust generated Scala to make it work with scalac -old-syntax and -new-syntax, although the latter is not regularly tested;
The file was modified src/Tools/Code/code_scala.ML (diff)
Changeset 80085:5c73934777fc by simon wimmer _wimmers@in.tum.de_:
Add entry on Sketch_and_Explore to CONTRIBUTORS
The file was modified CONTRIBUTORS (diff)