src/HOL/Isar_examples/ROOT.ML
changeset 8247 635339ef2dca
parent 8137 fb6fe34060ca
child 8675 a2ff2301d65e