src/HOL/Isar_examples/ROOT.ML
changeset 12791 ccc0f45ad2c4
parent 12105 1e4451999200
child 12946 75447c743810