src/HOL/Library/Realizers.thy
17 months ago blanchet 2018-01-02 moved 'realizers' into their own theory, now that they are decupled from the old datatype construction