equal
deleted
inserted
replaced
206 The subsequent commands help to reproduce the old forms, e.g. to |
206 The subsequent commands help to reproduce the old forms, e.g. to |
207 simplify porting old theories: |
207 simplify porting old theories: |
208 |
208 |
209 type_notation Map.map (infixr "~=>" 0) |
209 type_notation Map.map (infixr "~=>" 0) |
210 notation Map.map_comp (infixl "o'_m" 55) |
210 notation Map.map_comp (infixl "o'_m" 55) |
|
211 |
|
212 * The alternative notation "\<Colon>" for type and sort constraints has been |
|
213 removed: in LaTeX document output it looks the same as "::". |
|
214 INCOMPATIBILITY, use plain "::" instead. |
211 |
215 |
212 * Case combinator "prod_case" with eta-contracted body functions |
216 * Case combinator "prod_case" with eta-contracted body functions |
213 has explicit "uncurry" notation, to provide a compact notation while |
217 has explicit "uncurry" notation, to provide a compact notation while |
214 getting ride of a special case translation. Slight syntactic |
218 getting ride of a special case translation. Slight syntactic |
215 INCOMPATIBILITY. |
219 INCOMPATIBILITY. |