diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-19 09:13:45 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-19 09:13:45 +0000 |
| commit | d2f8cbfba4a1d5f9a2619ca83a26e315ebf71bfc (patch) | |
| tree | 46f4beb9aa9ef7a4834b1352de1bcb572b594be2 /test-suite/success/NatRing.v | |
| parent | 58767d7a26e9d72de1c01f8cf9a52a1afd454859 (diff) | |
NatRing
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2325 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/NatRing.v')
| -rw-r--r-- | test-suite/success/NatRing.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/success/NatRing.v b/test-suite/success/NatRing.v new file mode 100644 index 000000000..47d9f9b5a --- /dev/null +++ b/test-suite/success/NatRing.v @@ -0,0 +1,5 @@ +Require ArithRing. + +Goal (S (S O))=(plus (S O) (S O)). +NatRing. +Qed. |