src/HOL/hologic.ML
changeset 23024 70435ffe077d
parent 22994 02440636214f
child 23247 b99dce43d252