src/HOL/typedef.ML
changeset 3225 cee363fc07d7
parent 2934 bd922fc9001b
child 3768 67f4ac759100