Summary
- tuned proofs -- prefer explicit names for facts from 'interpret';
- merged
- eliminated questionable Par_List.map -- locale interpretation is mostly lazy (see also b81f1de9f57e);
- tuned signature;
- tuned;
- use lazy notes for locale context init and later additions of facts;
- avoid premature Lazy.force due to strict "?" operator;
The file was modified | src/HOL/Analysis/Brouwer_Fixpoint.thy (diff) |
The file was modified | src/HOL/Analysis/Caratheodory.thy (diff) |
The file was modified | src/HOL/Analysis/Derivative.thy (diff) |
The file was modified | src/HOL/HOLCF/ConvexPD.thy (diff) |
The file was modified | src/HOL/HOLCF/LowerPD.thy (diff) |
The file was modified | src/HOL/HOLCF/Map_Functions.thy (diff) |
The file was modified | src/HOL/HOLCF/UpperPD.thy (diff) |
The file was modified | src/HOL/Library/RBT_Set.thy (diff) |
The file was modified | src/HOL/Probability/Levy.thy (diff) |
The file was modified | src/Pure/Isar/locale.ML (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/Isar/locale.ML (diff) |
The file was modified | src/Pure/facts.ML (diff) |