src/HOL/Isar_examples/ROOT.ML
changeset 15485 e93a3badc2bc
parent 12946 75447c743810
child 16356 94011cf701a4