src/Pure/Tools/rule_insts.ML
changeset 65712 ddd6dfc28e80
parent 63120 629a4c5e953e
child 67147 dea94b1aabc3