src/HOL/ex/SVC_Oracle.ML
changeset 16835 2e7d7ec7a268
parent 15531 08c8dad8e399
child 16836 45a3dc4688bc