src/HOL/Isar_examples/ROOT.ML
changeset 9744 9ca034ef256c
parent 8814 0a5edcbe0695
child 9942 87f0809a06a9