equal
deleted
inserted
replaced
341 apply (clarsimp simp add : test_bit_bl word_size) |
341 apply (clarsimp simp add : test_bit_bl word_size) |
342 done |
342 done |
343 |
343 |
344 lemmas td_ext_nth = td_ext_nth' [OF refl refl refl, unfolded word_size] |
344 lemmas td_ext_nth = td_ext_nth' [OF refl refl refl, unfolded word_size] |
345 |
345 |
346 interpretation test_bit!: |
346 interpretation test_bit: |
347 td_ext "op !! :: 'a::len0 word => nat => bool" |
347 td_ext "op !! :: 'a::len0 word => nat => bool" |
348 set_bits |
348 set_bits |
349 "{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}" |
349 "{f. \<forall>i. f i \<longrightarrow> i < len_of TYPE('a::len0)}" |
350 "(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))" |
350 "(\<lambda>h i. h i \<and> i < len_of TYPE('a::len0))" |
351 by (rule td_ext_nth) |
351 by (rule td_ext_nth) |