src/HOL/HOL.ML
changeset 3477 3aced7fa7d8b
parent 3436 d68dbb8f22d3
child 3615 e5322197cfea