theory week09A_demo_records
imports Main
begin


record A = a :: nat
           b :: int

term "\<lparr>a = 3,b = 4\<rparr>"
term a
term b
term a_update

consts r :: A

term "a r"

consts re :: "unit A_scheme"
consts rf :: "int A_scheme"

term re
term rf

term "A.more"
term "A.more rf"

record B = A + c :: "nat list"

consts rb :: B
term rb
term "A.a rb"
term B.more
term A.more

end