changeset 34971 | 5c290f56ebf7 |
parent 33613 | ad27f52ee759 |
child 37826 | 4c0a5e35931a |
--- 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 -