(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/tests/paramodulation".
-include "../legacy/coq.ma".
+
+include "coq.ma".
alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
alias symbol "eq" (instance 0) = "Coq's leibnitz's equality".
alias symbol "plus" (instance 0) = "Coq's natural plus".
-alias num (instance 0) = "natural number".
+alias num (instance 0) = "Coq natural number".
alias symbol "times" (instance 0) = "Coq's natural times".
theorem para1:
\forall n,m,n1,m1:nat.
n=m \to n1 = m1 \to (n + n1) = (m + m1).
-intros. auto paramodulation.
+intros. autobatch paramodulation.
qed.
theorem para2:
\forall n:nat. n + n = 2 * n.
-intros. auto paramodulation.
+intros. autobatch paramodulation library.
qed.