]> matita.cs.unibo.it Git - helm.git/blob - matita/tests/interactive/drop.ma
Two tests used to have the same baseuri. Very bad.
[helm.git] / matita / tests / interactive / drop.ma
1 set "baseuri" "cic:/matita/tests/drop".
2
3 alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
4 alias num (instance 0) = "natural number".
5 alias symbol "eq" (instance 0) = "leibnitz's equality".
6 alias symbol "plus" (instance 0) = "natural plus".
7 theorem a : O + 1 = 1.
8 drop.