src/HOL/Hoare_Parallel/RG_Examples.thy
Fri, 06 Dec 2024 13:33:25 +0100 wenzelm clarified printing of consts: rename apart from all bounds, and thus avoid old Term.declare_free_names with its adhoc policy ("as they are printed");
less more (0) -10 -1 tip