From 9a960326e6cbdc9f21d35843d55ea5593ffe0c1b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 Jun 2005 14:20:06 +0000 Subject: [PATCH] fix --- helm/matita/tests/auto.ma | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100755 helm/matita/tests/auto.ma diff --git a/helm/matita/tests/auto.ma b/helm/matita/tests/auto.ma new file mode 100755 index 000000000..22d849790 --- /dev/null +++ b/helm/matita/tests/auto.ma @@ -0,0 +1,10 @@ +alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". +alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)". +alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". +alias symbol "eq" (instance 0) = "leibnitz's equality". +alias symbol "minus" (instance 0) = "natural minus". +alias symbol "plus" (instance 0) = "natural plus". +alias symbol "times" (instance 0) = "natural times". +theorem a : \forall x,y:nat. x*x+(S y) = O - x. +intros. +auto 3. \ No newline at end of file -- 2.39.2