equal
deleted
inserted
replaced
5 *) |
5 *) |
6 |
6 |
7 section \<open>Saturated arithmetic\<close> |
7 section \<open>Saturated arithmetic\<close> |
8 |
8 |
9 theory Saturated |
9 theory Saturated |
10 imports Numeral_Type "~~/src/HOL/Word/Type_Length" |
10 imports Numeral_Type Type_Length |
11 begin |
11 begin |
12 |
12 |
13 subsection \<open>The type of saturated naturals\<close> |
13 subsection \<open>The type of saturated naturals\<close> |
14 |
14 |
15 typedef (overloaded) ('a::len) sat = "{.. len_of TYPE('a)}" |
15 typedef (overloaded) ('a::len) sat = "{.. len_of TYPE('a)}" |