src/HOL/Types_To_Sets/internalize_sort.ML
changeset 66061 880db47fed30
parent 64551 79e9587dbcca
child 69597 ff784d5a5bfb
equal deleted inserted replaced
66060:b2bfbefd354f 66061:880db47fed30