<?php /// $Id$

$string['filtername'] = "TeX Notation";

?>