# HG changeset patch
# User nipkow
# Date 1363084291 -3600
# Node ID df0f306f030f49859cf66852d63131d475873838
# Parent  635562bc14effad86180057262d653f3d5e4ac41
added pairs

diff -r 635562bc14ef -r df0f306f030f src/Doc/ProgProve/Types_and_funs.thy
--- a/src/Doc/ProgProve/Types_and_funs.thy	Tue Mar 12 07:51:10 2013 +0100
+++ b/src/Doc/ProgProve/Types_and_funs.thy	Tue Mar 12 11:31:31 2013 +0100
@@ -91,6 +91,10 @@
 
 text{*
 Note that @{text"\<tau>\<^isub>1 * \<tau>\<^isub>2"} is the type of pairs, also written @{text"\<tau>\<^isub>1 \<times> \<tau>\<^isub>2"}.
+Pairs can be taken apart either by pattern matching (as above) or with the
+projection functions @{const fst} and @{const snd}: @{thm fst_conv} and @{thm snd_conv}. Tuples are simulated by pairs nested to the right: @{term"(a,b,c)"}
+abbreviates @{text"(a, (b, c))"} and @{text "\<tau>\<^isub>1 \<times> \<tau>\<^isub>2 \<times> \<tau>\<^isub>3"} abbreviates
+@{text "\<tau>\<^isub>1 \<times> (\<tau>\<^isub>2 \<times> \<tau>\<^isub>3)"}.
 
 \subsection{Definitions}