From fc9cad6c109e279130501114000edcfb9621075b Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 27 Jun 2005 13:43:55 +0000 Subject: [PATCH] New syntax of auto: auto [depth = n] [width = m]. --- helm/matita/tests/auto.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/matita/tests/auto.ma b/helm/matita/tests/auto.ma index 22d849790..80256c0f4 100755 --- a/helm/matita/tests/auto.ma +++ b/helm/matita/tests/auto.ma @@ -7,4 +7,4 @@ 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 +auto depth = 3. -- 2.39.2