src/HOL/Library/Realizers.thy
Tue, 02 Jan 2018 16:17:13 +0100 blanchet moved 'realizers' into their own theory, now that they are decupled from the old datatype construction
less more (0) tip