equal
deleted
inserted
replaced
112 |
112 |
113 lemma [code func]: |
113 lemma [code func]: |
114 "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of_index k) (nat_of_index l)" |
114 "eq_class.eq k l \<longleftrightarrow> eq_class.eq (nat_of_index k) (nat_of_index l)" |
115 by (cases k, cases l) (simp add: eq) |
115 by (cases k, cases l) (simp add: eq) |
116 |
116 |
|
117 lemma [code nbe]: |
|
118 "eq_class.eq (k::index) k \<longleftrightarrow> True" |
|
119 by (rule HOL.eq_refl) |
|
120 |
117 |
121 |
118 subsection {* Indices as datatype of ints *} |
122 subsection {* Indices as datatype of ints *} |
119 |
123 |
120 instantiation index :: number |
124 instantiation index :: number |
121 begin |
125 begin |