equal
deleted
inserted
replaced
35 "_State ms" == "_Update <> ms" |
35 "_State ms" == "_Update <> ms" |
36 |
36 |
37 text {* \noindent |
37 text {* \noindent |
38 We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly: |
38 We can now write a series of updates to the function @{text "\<lambda>x. 0"} compactly: |
39 *} |
39 *} |
40 lemma "<a := Suc 0, b := 2> = (<> (a := Suc 0)) (b := 2)" |
40 lemma "<a := 1, b := 2> = (<> (a := 1)) (b := (2::int))" |
41 by (rule refl) |
41 by (rule refl) |
42 |
42 |
43 value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>" |
43 value "aval (Plus (V ''x'') (N 5)) <''x'' := 7>" |
44 |
44 |
45 |
45 |