# HG changeset patch
# User haftmann
# Date 1264597373 -3600
# Node ID 5c290f56ebf7bb5b0e1261d4d71f0131c48bc5da
# Parent  4c316d777461bb5979e98fb08c4ebaf5532122d6
a more complex record expression -- cf. src/HOL/Tools/quickcheck_generators.ML

diff -r 4c316d777461 -r 5c290f56ebf7 src/HOL/ex/Records.thy
--- a/src/HOL/ex/Records.thy	Wed Jan 27 14:02:53 2010 +0100
+++ b/src/HOL/ex/Records.thy	Wed Jan 27 14:02:53 2010 +0100
@@ -334,6 +334,16 @@
   done
 
 
+subsection {* A more complex record expression *}
+
+record ('a, 'b, 'c) bar = bar1 :: 'a
+  bar2 :: 'b
+  bar3 :: 'c
+  bar21 :: "'b \<times> 'a"
+  bar32 :: "'c \<times> 'b"
+  bar31 :: "'c \<times> 'a"
+
+
 subsection {* Some code generation *}
 
 export_code foo1 foo3 foo5 foo10 foo11 in SML file -