doc-src/HOL/HOL-rules.txt
changeset 11944 0594e63e6057
parent 6580 ff2c3ffd38ee