equal
deleted
inserted
replaced
143 are generated into companion object of corresponding type class, to resolve |
143 are generated into companion object of corresponding type class, to resolve |
144 some situations where ambiguities may occur. |
144 some situations where ambiguities may occur. |
145 |
145 |
146 |
146 |
147 *** HOL *** |
147 *** HOL *** |
|
148 |
|
149 * Theory Set_Interval.thy: substantial new theorems on indexed sums |
|
150 and products. |
148 |
151 |
149 * Theory Library/LaTeXsugar.thy: New style "dummy_pats" for displaying |
152 * Theory Library/LaTeXsugar.thy: New style "dummy_pats" for displaying |
150 equations in functional programming style: variables present on the |
153 equations in functional programming style: variables present on the |
151 left-hand but not on the righ-hand side are replaced by underscores. |
154 left-hand but not on the righ-hand side are replaced by underscores. |
152 |
155 |