src/HOL/Tools/datatype_realizer.ML
changeset 15298 a5bea99352d6
parent 15256 9237f388fbb1
child 15531 08c8dad8e399
equal deleted inserted replaced
15297:0aff5d912422 15298:a5bea99352d6