src/HOL/Tools/typedef.ML
changeset 56065 600781e03bf6
parent 54883 dd04a8b654fc
child 56375 32e0da92c786
equal deleted inserted replaced
56064:7658489047e3 56065:600781e03bf6