equal
deleted
inserted
replaced
1 (* Title: HOL/Library/Ref.thy |
1 (* Title: HOL/Library/Ref.thy |
2 ID: $Id$ |
|
3 Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen |
2 Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen |
4 *) |
3 *) |
5 |
4 |
6 header {* Monadic references *} |
5 header {* Monadic references *} |
7 |
6 |
51 by (cases f) |
50 by (cases f) |
52 (auto simp add: Let_def bindM_def lookup_def expand_fun_eq) |
51 (auto simp add: Let_def bindM_def lookup_def expand_fun_eq) |
53 |
52 |
54 lemma update_change [code]: |
53 lemma update_change [code]: |
55 "r := e = Ref.change (\<lambda>_. e) r \<guillemotright> return ()" |
54 "r := e = Ref.change (\<lambda>_. e) r \<guillemotright> return ()" |
56 by (auto simp add: monad_simp change_def lookup_chain) |
55 by (auto simp add: change_def lookup_chain) |
57 |
56 |
58 |
57 |
59 subsection {* Code generator setup *} |
58 subsection {* Code generator setup *} |
60 |
59 |
61 subsubsection {* SML *} |
60 subsubsection {* SML *} |