From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 24 May 2005 13:34:02 +0000 (+0000)
Subject: added simpl test script
X-Git-Tag: single_binding~13
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=03b76418d261acfb3b33d64283ea0269ba596859;p=helm.git

added simpl test script
---

diff --git a/helm/matita/tests/simpl.ma b/helm/matita/tests/simpl.ma
new file mode 100644
index 000000000..887566f58
--- /dev/null
+++ b/helm/matita/tests/simpl.ma
@@ -0,0 +1,8 @@
+alias id "not" = "cic:/Coq/Init/Logic/not.con".
+alias symbol "eq" (instance 0) = "leibnitz's equality".
+theorem a : 
+ \forall A:Set.
+ \forall x,y : A.
+ not (x = y) \to not(y = x).
+intro.
+simplify in hyp not(x=y).