Summary
- merged
- tuned;
- merged
- code_target: create subdirectories for export_code file
- clarified signature: support "suppress" prefix as int, followed by list;
- minor performance tuning: more elementary operations;
- tuned signature;
- minor performance tuning: more elementary operations;
- tuned signature;
- more operations;
The file was modified | src/Pure/General/long_name.ML (diff) |
The file was modified | src/Pure/General/name_space.ML (diff) |
The file was modified | src/Tools/Code/code_target.ML (diff) |
The file was modified | src/Pure/General/long_name.ML (diff) |
The file was modified | src/Pure/General/long_name.ML (diff) |
The file was modified | src/Pure/General/long_name.ML (diff) |
The file was modified | src/Pure/General/long_name.ML (diff) |
The file was modified | src/Pure/General/long_name.ML (diff) |
The file was modified | src/Pure/General/name_space.ML (diff) |
The file was modified | src/Pure/Tools/find_theorems.ML (diff) |
The file was modified | src/Pure/General/vector.ML (diff) |