src/HOL/typedef.ML
changeset 3721 12409b467fae
parent 2934 bd922fc9001b
child 3768 67f4ac759100