src/Pure/Tools/rule_insts.ML
changeset 65534 b6250ee6ce79
parent 63120 629a4c5e953e
child 67147 dea94b1aabc3
equal deleted inserted replaced
65533:4a7e794944df 65534:b6250ee6ce79