diff --git a/autotests/folding/test.mm.fold b/autotests/folding/test.mm.fold
new file mode 100644
--- /dev/null
+++ b/autotests/folding/test.mm.fold
@@ -0,0 +1,42 @@
+$( Modified version of demo0.mm from 1-Jan-04 $)
+
+$(
+ PUBLIC DOMAIN DEDICATION
+
+This file is placed in the public domain per the Creative Commons Public
+Domain Dedication. http://creativecommons.org/licenses/publicdomain/
+
+Norman Megill - email: nm at alum.mit.edu
+$)
+
+$c 0 + = -> ( ) term wff |- $.
+
+$v t r s P Q $.
+
+tt $f term t $.
+tr $f term r $.
+ts $f term s $.
+wp $f wff P $.
+wq $f wff Q $.
+
+tze $a term 0 $.
+tpl $a term ( t + r ) $.
+
+weq $a wff t = r $.
+wim $a wff ( P -> Q ) $.
+
+a1 $a |- ( t = r -> ( t = s -> r = s ) ) $.
+a2 $a |- ( t + 0 ) = t $.
+${
+ $( Define the modus ponens inference rule $)
+ min $e |- P $.
+ maj $e |- ( P -> Q ) $.
+ mp $a |- Q $.
+$}
+
+th1 $p |- t = t $=
+ $( Here is its proof: $)
+ tt tze tpl tt weq tt tt weq tt a2 tt tze tpl
+ tt weq tt tze tpl tt weq tt tt weq wim tt a2
+ tt tze tpl tt tt a1 mp mp
+$.
diff --git a/autotests/html/test.mm.html b/autotests/html/test.mm.html
new file mode 100644
--- /dev/null
+++ b/autotests/html/test.mm.html
@@ -0,0 +1,49 @@
+
+
+
+test.mm
+
+
+$( Modified version of demo0.mm from 1-Jan-04 $)
+
+$(
+ PUBLIC DOMAIN DEDICATION
+
+This file is placed in the public domain per the Creative Commons Public
+Domain Dedication. http://creativecommons.org/licenses/publicdomain/
+
+Norman Megill - email: nm at alum.mit.edu
+$)
+
+$c 0 + = -> ( ) term wff |- $.
+
+$v t r s P Q $.
+
+tt$fterm t $.
+tr$fterm r $.
+ts$fterm s $.
+wp$fwff P $.
+wq$fwff Q $.
+
+tze$aterm 0 $.
+tpl$aterm ( t + r ) $.
+
+weq$awff t = r $.
+wim$awff ( P -> Q ) $.
+
+a1$a|- ( t = r -> ( t = s -> r = s ) ) $.
+a2$a|- ( t + 0 ) = t $.
+${
+ $( Define the modus ponens inference rule $)
+ min$e|- P $.
+ maj$e|- ( P -> Q ) $.
+ mp$a|- Q $.
+$}
+
+th1$p|- t = t $=
+$( Here is its proof: $)
+ tt tze tpl tt weq tt tt weq tt a2 tt tze tpl
+ tt weq tt tze tpl tt weq tt tt weq wim tt a2
+ tt tze tpl tt tt a1 mp mp
+$.
+
diff --git a/autotests/input/test.mm b/autotests/input/test.mm
new file mode 100644
--- /dev/null
+++ b/autotests/input/test.mm
@@ -0,0 +1,42 @@
+$( Modified version of demo0.mm from 1-Jan-04 $)
+
+$(
+ PUBLIC DOMAIN DEDICATION
+
+This file is placed in the public domain per the Creative Commons Public
+Domain Dedication. http://creativecommons.org/licenses/publicdomain/
+
+Norman Megill - email: nm at alum.mit.edu
+$)
+
+$c 0 + = -> ( ) term wff |- $.
+
+$v t r s P Q $.
+
+tt $f term t $.
+tr $f term r $.
+ts $f term s $.
+wp $f wff P $.
+wq $f wff Q $.
+
+tze $a term 0 $.
+tpl $a term ( t + r ) $.
+
+weq $a wff t = r $.
+wim $a wff ( P -> Q ) $.
+
+a1 $a |- ( t = r -> ( t = s -> r = s ) ) $.
+a2 $a |- ( t + 0 ) = t $.
+${
+ $( Define the modus ponens inference rule $)
+ min $e |- P $.
+ maj $e |- ( P -> Q ) $.
+ mp $a |- Q $.
+$}
+
+th1 $p |- t = t $=
+ $( Here is its proof: $)
+ tt tze tpl tt weq tt tt weq tt a2 tt tze tpl
+ tt weq tt tze tpl tt weq tt tt weq wim tt a2
+ tt tze tpl tt tt a1 mp mp
+$.
diff --git a/autotests/input/test.mm.syntax b/autotests/input/test.mm.syntax
new file mode 100644
--- /dev/null
+++ b/autotests/input/test.mm.syntax
@@ -0,0 +1 @@
+Metamath
diff --git a/autotests/reference/test.mm.ref b/autotests/reference/test.mm.ref
new file mode 100644
--- /dev/null
+++ b/autotests/reference/test.mm.ref
@@ -0,0 +1,42 @@
+$( Modified version of demo0.mm from 1-Jan-04 $)
+
+$(
+ PUBLIC DOMAIN DEDICATION
+
+This file is placed in the public domain per the Creative Commons Public
+Domain Dedication. http://creativecommons.org/licenses/publicdomain/
+
+Norman Megill - email: nm at alum.mit.edu
+$)
+
+$c 0 + = -> ( ) term wff |- $.
+
+$v t r s P Q $.
+
+$fterm t $.
+$fterm r $.
+$fterm s $.
+$fwff P $.
+$fwff Q $.
+
+$aterm 0 $.
+$aterm ( t + r ) $.
+
+$awff t = r $.
+$awff ( P -> Q ) $.
+
+$a|- ( t = r -> ( t = s -> r = s ) ) $.
+$a|- ( t + 0 ) = t $.
+${
+$( Define the modus ponens inference rule $)
+$e|- P $.
+$e|- ( P -> Q ) $.
+$a|- Q $.
+$}
+
+$p|- t = t $=
+$( Here is its proof: $)
+
+
+
+$.
diff --git a/data/syntax/metamath.xml b/data/syntax/metamath.xml
new file mode 100644
--- /dev/null
+++ b/data/syntax/metamath.xml
@@ -0,0 +1,122 @@
+
+
+
+]>
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+