equal
deleted
inserted
replaced
83 |
83 |
84 |
84 |
85 text \<open>Syntactic convenience\<close> |
85 text \<open>Syntactic convenience\<close> |
86 |
86 |
87 setup \<open> |
87 setup \<open> |
88 Sign.add_const_constraint (@{const_name Array}, SOME @{typ "nat \<Rightarrow> 'a::heap array"}) |
88 Sign.add_const_constraint (\<^const_name>\<open>Array\<close>, SOME \<^typ>\<open>nat \<Rightarrow> 'a::heap array\<close>) |
89 #> Sign.add_const_constraint (@{const_name Ref}, SOME @{typ "nat \<Rightarrow> 'a::heap ref"}) |
89 #> Sign.add_const_constraint (\<^const_name>\<open>Ref\<close>, SOME \<^typ>\<open>nat \<Rightarrow> 'a::heap ref\<close>) |
90 #> Sign.add_const_constraint (@{const_name addr_of_array}, SOME @{typ "'a::heap array \<Rightarrow> nat"}) |
90 #> Sign.add_const_constraint (\<^const_name>\<open>addr_of_array\<close>, SOME \<^typ>\<open>'a::heap array \<Rightarrow> nat\<close>) |
91 #> Sign.add_const_constraint (@{const_name addr_of_ref}, SOME @{typ "'a::heap ref \<Rightarrow> nat"}) |
91 #> Sign.add_const_constraint (\<^const_name>\<open>addr_of_ref\<close>, SOME \<^typ>\<open>'a::heap ref \<Rightarrow> nat\<close>) |
92 \<close> |
92 \<close> |
93 |
93 |
94 hide_const (open) empty |
94 hide_const (open) empty |
95 |
95 |
96 end |
96 end |