src/Pure/defs.ML
changeset 17445 3c9c46b820f5
parent 17412 e26cb20ef0cc
child 17669 94dbbffbf94b