From: Claudio Sacerdoti Coen Date: Wed, 15 Jun 2005 12:15:26 +0000 (+0000) Subject: ... X-Git-Tag: PRE_STORAGE~10 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7d5438513549fb3b1e7ba39d095db00b99478eaf;p=helm.git ... --- diff --git a/helm/matita/tests/coercions.ma b/helm/matita/tests/coercions.ma index 8a45f2929..337ef50ed 100644 --- a/helm/matita/tests/coercions.ma +++ b/helm/matita/tests/coercions.ma @@ -29,10 +29,3 @@ alias symbol "eq" (instance 0) = "leibnitz's equality". theorem a: fst O one = fst (positive O) (next one). reflexivity. qed. - - - - - - -