src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
Tue, 22 Apr 2025 19:02:33 +0200 Manuel Eberl dropped problematic code equation for multisets for RBT code testing
Thu, 11 Aug 2022 11:57:19 +0200 nipkow nlists is picked up automatically but conflicts with the RBT setup
Mon, 28 Jun 2021 20:10:23 +0200 Andreas Lochbihler move code setup from Cardinality to separate theory
less more (0) -10 -3 tip