src/HOL/Isar_examples/ROOT.ML
changeset 7990 0a604b2fc2b1
parent 7800 8ee919e42174
child 8020 2823ce1753a5