src/HOL/Isar_examples/ROOT.ML
changeset 16530 3e493fa130a3
parent 16356 94011cf701a4
child 19021 0111ecc5490e