src/Pure/ML/ml_thms.ML
changeset 77287 d060545f01a2
parent 74606 40f5c6b2e8aa
child 78795 f7e972d567f3