(* *)
(****************************************************************************)
-set "baseuri" "cic:/matita/tests/".
+set "baseuri" "cic:/matita/tests/comments/".
(* commento che va nell'ast, ma non viene contato
come step perche' non e' un executable
*)
alias num (instance 0) = "natural number".
-alias symbol "eq" (instance 0) = "leibnitz's equality".
+alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
theorem a:0=0.
(* nota *)