src/HOL/ex/svc_oracle.ML
changeset 21966 edab0ecfbd7c
parent 20817 7ec9b692183c
child 22997 d4f3b015b50b