src/HOL/Tools/datatype_realizer.ML
changeset 17040 6682c93b7d9f
parent 16123 1381e90c2694
child 17521 0f1c48de39f5
equal deleted inserted replaced
17039:78159411623f 17040:6682c93b7d9f