Creating Latex Output from Agda Files

If one has installed Alfa and latex, one can create nice Latex output from Agda as follows:
Replace '_dot_' by '.' and '_at_' by '@' in 'a_dot_g_dot_setzer_at_swan_dot_ac_dot_uk'
Last modified: Thu Jan 22 00:57:42 GMT 2004