src/Pure/Tools/rule_insts.ML
changeset 66717 67dbf5cdc056
parent 63120 629a4c5e953e
child 67147 dea94b1aabc3
equal deleted inserted replaced
66716:8737b866bd1c 66717:67dbf5cdc056