src/Pure/ML/ml_thms.ML
changeset 62337 d3996d5873dd
parent 61814 1ca1142e1711
child 62876 507c90523113