src/Pure/defs.ML
changeset 16122 864fda4a4056
parent 16113 692fe6595755
child 16158 2c3565b74b7a