| changeset 66453 | cc19f7ca2ed6 |
| parent 63190 | 3e79279c10ca |
| 66452:450cefec7c11 | 66453:cc19f7ca2ed6 |
|---|---|
7 *) |
7 *) |
8 |
8 |
9 section \<open>Tests Type Class Instances as Friends\<close> |
9 section \<open>Tests Type Class Instances as Friends\<close> |
10 |
10 |
11 theory Type_Class |
11 theory Type_Class |
12 imports "~~/src/HOL/Library/BNF_Corec" "~~/src/HOL/Library/Stream" |
12 imports "HOL-Library.BNF_Corec" "HOL-Library.Stream" |
13 begin |
13 begin |
14 |
14 |
15 instantiation stream :: (plus) plus |
15 instantiation stream :: (plus) plus |
16 begin |
16 begin |
17 |
17 |