equal
deleted
inserted
replaced
16 |
16 |
17 text {* See @{file "Examples/WordExamples.thy"} for examples. *} |
17 text {* See @{file "Examples/WordExamples.thy"} for examples. *} |
18 |
18 |
19 subsection {* Type definition *} |
19 subsection {* Type definition *} |
20 |
20 |
21 typedef '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 |
23 |
23 |
24 lemma uint_nonnegative: |
24 lemma uint_nonnegative: |
25 "0 \<le> uint w" |
25 "0 \<le> uint w" |
26 using word.uint [of w] by simp |
26 using word.uint [of w] by simp |