src/Pure/Tools/plugin.ML
changeset 77505 7ee426daafa3
parent 74563 042041c0ebeb
child 78795 f7e972d567f3
equal deleted inserted replaced
77504:fd40e36045fd 77505:7ee426daafa3