src/Pure/Build/export_theory.ML
Sat, 30 Nov 2024 13:41:38 +0100 wenzelm tuned: more direct use of Name.context operations;
less more (0) -10 -1 tip