equal
deleted
inserted
replaced
90 be stripped in ML translations via Syntax.strip_positions / |
90 be stripped in ML translations via Syntax.strip_positions / |
91 Syntax.strip_positions_ast, or via the syntax constant |
91 Syntax.strip_positions_ast, or via the syntax constant |
92 "_strip_positions" within parse trees. As last resort, positions can |
92 "_strip_positions" within parse trees. As last resort, positions can |
93 be disabled via the configuration option Syntax.positions, which is |
93 be disabled via the configuration option Syntax.positions, which is |
94 called "syntax_positions" in Isar attribute syntax. |
94 called "syntax_positions" in Isar attribute syntax. |
|
95 |
|
96 * Discontinued special treatment of structure Ast: no pervasive |
|
97 content, no inclusion in structure Syntax. INCOMPATIBILITY, refer to |
|
98 qualified names like Ast.Constant etc. |
95 |
99 |
96 |
100 |
97 |
101 |
98 New in Isabelle2011 (January 2011) |
102 New in Isabelle2011 (January 2011) |
99 ---------------------------------- |
103 ---------------------------------- |