src/Pure/ML/ml_thms.ML
changeset 77817 a1bf8f706bc1
parent 74606 40f5c6b2e8aa
child 78795 f7e972d567f3