Summary
- more abbrevs -- this makes "(=" ambiguous and thus simplifies input of "(=)" (within the context of Main HOL);
- tuned -- more uniform;
- eliminated somewhat pointless parallelism (from 857da80611ab): usually hundreds of tasks with < 1ms each, also note that the enclosing join_theory happens within theory graph parallelism;
- Drop rewrite rule arguments of sublocale and interpretation implementations.
The file was modified | src/HOL/Library/Finite_Map.thy (diff) |
The file was modified | src/HOL/Map.thy (diff) |
The file was modified | src/Pure/Isar/proof_context.ML (diff) |
The file was modified | src/Pure/global_theory.ML (diff) |
The file was modified | src/Pure/more_thm.ML (diff) |
The file was modified | src/HOL/Statespace/state_space.ML (diff) |
The file was modified | src/Pure/Isar/interpretation.ML (diff) |
The file was modified | src/Pure/Pure.thy (diff) |