Summary
- lifting setup for char
- 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
- uniform namespace handling for both concrete and abstract types, following 32e0da92c786
- clarified
- corrected slip
- tuned
- work around weakness in export calculation when generating OCaml code
- tuned
The file was modified | src/HOL/String.thy (diff) |
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) |
The file was modified | src/Pure/Isar/code.ML (diff) |
The file was modified | src/Pure/Isar/code.ML (diff) |
The file was modified | src/Tools/Code/code_scala.ML (diff) |
The file was modified | src/Tools/Code/code_ml.ML (diff) |
The file was modified | src/Tools/Code/code_scala.ML (diff) |
The file was modified | src/Tools/Code/code_ml.ML (diff) |
The file was modified | src/Pure/Isar/code.ML (diff) |