src/Pure/Tools/rule_insts.ML
changeset 60916 a6e2a667b0a8
parent 60695 757549b4bbe6
child 61841 4d3527b94f2a