src/HOL/Isar_examples/ROOT.ML
changeset 31106 9a1178204dc0
parent 24228 9e2234f2aff1
child 31758 3edd5f813f01