src/Pure/context.ML
changeset 60916 a6e2a667b0a8
parent 59163 857a600f0c94
child 60947 d5f7b424ba47