summaryrefslogtreecommitdiff
path: root/theories/ZArith/intro.tex
diff options
context:
space:
mode:
Diffstat (limited to 'theories/ZArith/intro.tex')
-rwxr-xr-xtheories/ZArith/intro.tex6
1 files changed, 6 insertions, 0 deletions
diff --git a/theories/ZArith/intro.tex b/theories/ZArith/intro.tex
new file mode 100755
index 00000000..21e52c19
--- /dev/null
+++ b/theories/ZArith/intro.tex
@@ -0,0 +1,6 @@
+\section{Binary integers : ZArith}
+The {\tt ZArith} library deals with binary integers (those used
+by the {\tt Omega} decision tactic).
+Here are defined various arithmetical notions and their properties,
+similar to those of {\tt Arith}.
+