Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. lifting setup for char
  2. one single plugin for code type declarations avoids problems when bootstrapping new plugins over types which have been both declared concrete and abstract in their code historiy
  3. uniform namespace handling for both concrete and abstract types, following 32e0da92c786
  4. clarified
  5. corrected slip
  6. tuned
  7. work around weakness in export calculation when generating OCaml code
  8. tuned
Changeset 66331:f773691617c0 by haftmann:
lifting setup for char
The file was modified src/HOL/String.thy (diff)
Changeset 66330:dcb3e6bdc00a by haftmann:
one single plugin for code type declarations avoids problems when bootstrapping new plugins over types which have been both declared concrete and abstract in their code historiy
The file was modified src/HOL/Tools/code_evaluation.ML (diff)
The file was modified src/HOL/Typerep.thy (diff)
The file was modified src/Pure/Isar/code.ML (diff)
Changeset 66329:a0369be63948 by haftmann:
uniform namespace handling for both concrete and abstract types, following 32e0da92c786
The file was modified src/Pure/Isar/code.ML (diff)
Changeset 66328:cf9ce8016da1 by haftmann:
clarified
The file was modified src/Pure/Isar/code.ML (diff)
Changeset 66327:f44f7cf3d1a1 by haftmann:
corrected slip
The file was modified src/Tools/Code/code_scala.ML (diff)
Changeset 66326:9eb8a2d07852 by haftmann:
tuned
The file was modified src/Tools/Code/code_ml.ML (diff)
The file was modified src/Tools/Code/code_scala.ML (diff)
Changeset 66325:fd28cb6e6f2c by haftmann:
work around weakness in export calculation when generating OCaml code
The file was modified src/Tools/Code/code_ml.ML (diff)
Changeset 66324:859b66d75dff by haftmann:
tuned
The file was modified src/Pure/Isar/code.ML (diff)