aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--theories/NArith/intro.tex5
-rw-r--r--theories/Setoids/intro.tex1
-rw-r--r--theories/Sorting/intro.tex1
3 files changed, 7 insertions, 0 deletions
diff --git a/theories/NArith/intro.tex b/theories/NArith/intro.tex
new file mode 100644
index 000000000..83eed970e
--- /dev/null
+++ b/theories/NArith/intro.tex
@@ -0,0 +1,5 @@
+\section{Binary positive and non negative integers : NArith}\label{NArith}
+
+Here are defined various arithmetical notions and their properties,
+similar to those of {\tt Arith}.
+
diff --git a/theories/Setoids/intro.tex b/theories/Setoids/intro.tex
new file mode 100644
index 000000000..50cd025de
--- /dev/null
+++ b/theories/Setoids/intro.tex
@@ -0,0 +1 @@
+\section{Setoids}\label{Setoids}
diff --git a/theories/Sorting/intro.tex b/theories/Sorting/intro.tex
new file mode 100644
index 000000000..64ae4c888
--- /dev/null
+++ b/theories/Sorting/intro.tex
@@ -0,0 +1 @@
+\section{Sorting}\label{Sorting}