| changeset 67965 | aaa31cd0caef |
| parent 67964 | 08cc5ab18c84 |
| child 68020 | 6aade817bee5 |
| 67964:08cc5ab18c84 | 67965:aaa31cd0caef |
|---|---|
3 section \<open>1-2 Brother Tree Implementation of Sets\<close> |
3 section \<open>1-2 Brother Tree Implementation of Sets\<close> |
4 |
4 |
5 theory Brother12_Set |
5 theory Brother12_Set |
6 imports |
6 imports |
7 Cmp |
7 Cmp |
8 Set_Interfaces |
8 Set_Specs |
9 "HOL-Number_Theory.Fib" |
9 "HOL-Number_Theory.Fib" |
10 begin |
10 begin |
11 |
11 |
12 subsection \<open>Data Type and Operations\<close> |
12 subsection \<open>Data Type and Operations\<close> |
13 |
13 |