src/HOL/Tools/Old_Datatype/old_size.ML
changeset 64990 c6a7de505796
parent 63239 d562c9948dee
child 66251 cd935b7cb3fb
equal deleted inserted replaced
64989:40c36a4aee1f 64990:c6a7de505796