--- a/src/Pure/context.ML Sat Aug 16 16:29:20 2025 +0200
+++ b/src/Pure/context.ML Sat Aug 16 16:34:41 2025 +0200
@@ -1,14 +1,19 @@
(* Title: Pure/context.ML
- Author: Markus Wenzel, TU Muenchen
+ Author: Makarius
-Generic theory contexts with unique identity, arbitrarily typed data,
-monotonic development graph and history support. Generic proof
-contexts with arbitrarily typed data.
+Generic theory contexts with unique identity, arbitrarily typed data, and
+monotonic updates.
-Firm naming conventions:
+Generic proof contexts with arbitrarily typed data.
+
+Good names:
thy, thy', thy1, thy2: theory
ctxt, ctxt', ctxt1, ctxt2: Proof.context
context: Context.generic
+
+Bad names:
+ ctx: Proof.context
+ context: Proof.context
*)
signature BASIC_CONTEXT =