src/HOL/plain.ML
changeset 39950 f3c4849868b8
parent 37694 19e8b730ddeb
equal deleted inserted replaced
39949:186a3b447e0b 39950:f3c4849868b8