equal
deleted
inserted
replaced
77 |
77 |
78 instance ref :: (type) countable |
78 instance ref :: (type) countable |
79 by (rule countable_classI [of addr_of_ref]) simp |
79 by (rule countable_classI [of addr_of_ref]) simp |
80 |
80 |
81 instance array :: (type) heap .. |
81 instance array :: (type) heap .. |
|
82 |
82 instance ref :: (type) heap .. |
83 instance ref :: (type) heap .. |
83 |
84 |
84 |
85 |
85 text \<open>Syntactic convenience\<close> |
86 text \<open>Syntactic convenience\<close> |
86 |
87 |
87 setup \<open> |
88 setup \<open> |
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>\<open>Array\<close>, SOME \<^typ>\<open>nat \<Rightarrow> 'a::heap array\<close>) |
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>\<open>Ref\<close>, SOME \<^typ>\<open>nat \<Rightarrow> 'a::heap ref\<close>) |