added examples

[helm.git] / helm / matita / tests / test4.ma

diff --git a/helm/matita/tests/test4.ma b/helm/matita/tests/test4.ma
new file mode 100644 (file)
index 0000000..4d7b03c
--- /dev/null
+++ b/helm/matita/tests/test4.ma
@@ -0,0 +1,4 @@
+alias num (instance 0) = "natural number".
+alias symbol "eq" (instance 0) = "leibnitz's equality".
+theorem a:0=0.
+reflexivity.
\ No newline at end of file