src/HOL/Tools/datatype_realizer.ML
changeset 19008 14c1b2f5dda4
parent 18929 d81435108688
child 19806 f860b7a98445