Changes

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;

Changeset 67682:00c436488398 by wenzelm: tuned proofs -- prefer explicit names for facts from 'interpret';
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)
Changeset 67681:b5058ba95e32 by wenzelm: merged
Changeset 67680:175a070e9dd8 by wenzelm: eliminated questionable Par_List.map -- locale interpretation is mostly lazy (see also b81f1de9f57e);
The file was modified	`src/Pure/Isar/locale.ML` (diff)
Changeset 67679:8fd84fe1d60b by wenzelm: tuned signature;
The file was modified	`src/Pure/Isar/proof_context.ML` (diff)
Changeset 67678:b4db2e7e414e by wenzelm: tuned;
The file was modified	`src/Pure/global_theory.ML` (diff)
Changeset 67677:ac4b475fc8c3 by wenzelm: use lazy notes for locale context init and later additions of facts;
The file was modified	`src/Pure/Isar/locale.ML` (diff)
Changeset 67676:47ffe7184cdd by wenzelm: avoid premature Lazy.force due to strict "?" operator;
The file was modified	`src/Pure/facts.ML` (diff)