src/HOL/hologic.ML
changeset 15827 5fdf2d8dab9c
parent 15620 8ccdc8bc66a2
child 15945 08e8d3fb9343