equal
deleted
inserted
replaced
230 lemma nat_of_index_code [code]: |
230 lemma nat_of_index_code [code]: |
231 "nat_of_index i = nat_of_index_aux i 0" |
231 "nat_of_index i = nat_of_index_aux i 0" |
232 by (simp add: nat_of_index_aux_def) |
232 by (simp add: nat_of_index_aux_def) |
233 |
233 |
234 |
234 |
|
235 text {* Measure function (for termination proofs) *} |
|
236 |
|
237 lemma [measure_function]: "is_measure nat_of_index" by (rule is_measure_trivial) |
|
238 |
235 subsection {* ML interface *} |
239 subsection {* ML interface *} |
236 |
240 |
237 ML {* |
241 ML {* |
238 structure Index = |
242 structure Index = |
239 struct |
243 struct |