Warning: this is an htmlized version!
The original is across this link,
and the conversion rules are here.
#!/usr/bin/env lua51
-- dednames.lua - extract names of deductions
-- Example:
--   (find-dn4sh0 "echo '%: ^foo ^bar notthis ^plic' | ./dednames.lua")
--      ==> "$$\\ded{foo} \\qquad \\ded{bar} \\qquad \\ded{plic}$$"
-- Used by:
--   (find-dn4 "dednat4.el")

for li in io.lines() do
  if li:match("^%%:%s+%^") then
    -- PP(li)
    T = {}
    for word in li:gmatch("%S+") do
       -- PP(word)
       if word:sub(1, 1) == "^" then
         table.insert(T, "\\ded{"..word:sub(2).."}")
       end
     end
     -- PP(T)
     print("$$" .. table.concat(T, " \\qquad ") .. "$$")
  end
end