src/HOL/Datatype_Examples/Free_Idempotent_Monoid.thy
Tue, 09 Mar 2021 14:20:27 +0100 traytel generalized confluence-based subdistributivity theorem for quotients;
Mon, 24 Feb 2020 21:46:45 +0100 traytel lift BNF witnesses for quotients (unless better ones are specified by the user)
Sun, 19 Jan 2020 07:50:35 +0100 traytel new examples of BNF lifting across quotients using a new theory of confluence,
less more (0) tip