equal
deleted
inserted
replaced
12 Bits_Int |
12 Bits_Int |
13 Misc_Typedef |
13 Misc_Typedef |
14 Misc_Arithmetic |
14 Misc_Arithmetic |
15 begin |
15 begin |
16 |
16 |
17 text \<open>See \<^file>\<open>WordExamples.thy\<close> for examples.\<close> |
17 text \<open>See \<^file>\<open>Word_Examples.thy\<close> for examples.\<close> |
18 |
18 |
19 subsection \<open>Type definition\<close> |
19 subsection \<open>Type definition\<close> |
20 |
20 |
21 typedef (overloaded) 'a word = "{(0::int) ..< 2 ^ len_of TYPE('a::len0)}" |
21 typedef (overloaded) 'a word = "{(0::int) ..< 2 ^ len_of TYPE('a::len0)}" |
22 morphisms uint Abs_word by auto |
22 morphisms uint Abs_word by auto |