src/HOL/HOL_lemmas.ML
changeset 8771 026f37a86ea7
parent 8529 4656e8312ba9
child 8964 df06ec11bbfa