src/HOL/Isar_examples/ROOT.ML
changeset 9450 c97dba47e504
parent 8814 0a5edcbe0695
child 9942 87f0809a06a9