src/HOL/hologic.ML
changeset 12791 ccc0f45ad2c4
parent 12338 de0f4a63baa5
child 13640 993576f4de30