Summary
- split balance into two, clearer etc
- ML antiquotation for generated computations
The file was modified | src/HOL/Data_Structures/RBT.thy (diff) |
The file was modified | src/HOL/Data_Structures/RBT_Map.thy (diff) |
The file was modified | src/HOL/Data_Structures/RBT_Set.thy (diff) |
The file was added | src/HOL/ex/Computations.thy |
The file was modified | src/HOL/ROOT (diff) |
The file was modified | src/Tools/Code/code_runtime.ML (diff) |
The file was modified | src/Tools/Code/code_target.ML (diff) |