equal
deleted
inserted
replaced
118 by (rule thelubE) |
118 by (rule thelubE) |
119 qed |
119 qed |
120 |
120 |
121 subsection {* Collection of continuity rules *} |
121 subsection {* Collection of continuity rules *} |
122 |
122 |
123 ML {* |
123 named_theorems cont2cont "continuity intro rule" |
124 structure Cont2ContData = Named_Thms |
124 |
125 ( |
|
126 val name = @{binding cont2cont} |
|
127 val description = "continuity intro rule" |
|
128 ) |
|
129 *} |
|
130 |
|
131 setup Cont2ContData.setup |
|
132 |
125 |
133 subsection {* Continuity of basic functions *} |
126 subsection {* Continuity of basic functions *} |
134 |
127 |
135 text {* The identity function is continuous *} |
128 text {* The identity function is continuous *} |
136 |
129 |