src/HOL/Tools/typedef.ML
changeset 58426 cac802846ff1
parent 58239 1c5bc387bd4c
child 58662 5963cdbad926
equal deleted inserted replaced
58425:246985c6b20b 58426:cac802846ff1