src/HOL/Update.ML
changeset 5071 548f398d770b
parent 5070 c42429b3e2f2
child 5133 42a7fe39a63a