| changeset 17914 | 99ead7a7eb42 |
| parent 12338 | de0f4a63baa5 |
| child 27169 | 89d5f117add3 |
| 17913:4159e1523ad8 | 17914:99ead7a7eb42 |
|---|---|
1 (*<*)theory Overloading = Overloading1:(*>*) |
1 (*<*)theory Overloading imports Overloading1 begin(*>*) |
2 instance list :: (type)ordrel |
2 instance list :: (type)ordrel |
3 by intro_classes |
3 by intro_classes |
4 |
4 |
5 text{*\noindent |
5 text{*\noindent |
6 This \isacommand{instance} declaration can be read like the declaration of |
6 This \isacommand{instance} declaration can be read like the declaration of |