src/HOL/Tools/Old_Datatype/old_datatype_data.ML
changeset 61476 1884c40f1539
parent 59582 0fbed69ff081
child 69593 3dda49e08b9d
equal deleted inserted replaced
61475:5b58a17c440a 61476:1884c40f1539