From dabc48aa1af52f7c6726b07471a03cb9e35be91c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 28 Jun 2005 17:41:17 +0000 Subject: [PATCH] fix --- helm/matita/tests/interactive/drop.ma | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 helm/matita/tests/interactive/drop.ma diff --git a/helm/matita/tests/interactive/drop.ma b/helm/matita/tests/interactive/drop.ma new file mode 100644 index 000000000..e0e302eb9 --- /dev/null +++ b/helm/matita/tests/interactive/drop.ma @@ -0,0 +1,6 @@ +alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". +alias num (instance 0) = "natural number". +alias symbol "eq" (instance 0) = "leibnitz's equality". +alias symbol "plus" (instance 0) = "natural plus". +theorem a : O + 1 = 1. +drop. -- 2.39.2