src/HOL/Tools/typedef.ML
changeset 35615 61bb9f8af129
parent 35430 df2862dc23a8
child 35625 9c818cab0dd0
equal deleted inserted replaced
35614:d7afa8700622 35615:61bb9f8af129