src/Pure/Tools/rule_insts.ML
changeset 65317 b9f5cd845616
parent 63120 629a4c5e953e
child 67147 dea94b1aabc3