src/HOL/Tools/typedef.ML
changeset 69044 364c989edb49
parent 68264 bb9a3be6952a
child 69829 3bfa28b3a5b2
equal deleted inserted replaced
69043:57a76e4728ed 69044:364c989edb49