src/HOL/typedef.ML
changeset 2981 aa5aeb6467c6
parent 2934 bd922fc9001b
child 3768 67f4ac759100