src/HOL/hologic.ML
changeset 6914 ad689270a265
parent 6380 32fda1090a13
child 7073 a959b4391fd8