# HG changeset patch
# User kleing
# Date 1363085966 -3600
# Node ID bbb7639554dc18f9ef9ea3d4d32c44996bd4df96
# Parent  27bb849330eac7dbb156cf46c014fce7d86b9426# Parent  df0f306f030f49859cf66852d63131d475873838
merged

diff -r 27bb849330ea -r bbb7639554dc src/Doc/ProgProve/Types_and_funs.thy
--- a/src/Doc/ProgProve/Types_and_funs.thy	Tue Mar 12 11:59:02 2013 +0100
+++ b/src/Doc/ProgProve/Types_and_funs.thy	Tue Mar 12 11:59:26 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}