equal
deleted
inserted
replaced
130 Only the margin for document output may be changed, but not the global |
130 Only the margin for document output may be changed, but not the global |
131 pretty printing: that is 76 for plain console output, and adapted |
131 pretty printing: that is 76 for plain console output, and adapted |
132 dynamically in GUI front-ends. Implementations of document |
132 dynamically in GUI front-ends. Implementations of document |
133 antiquotations need to observe the margin explicitly according to |
133 antiquotations need to observe the margin explicitly according to |
134 Thy_Output.string_of_margin. Minor INCOMPATIBILITY. |
134 Thy_Output.string_of_margin. Minor INCOMPATIBILITY. |
|
135 |
|
136 * Specification of 'document_files' in the session ROOT file is |
|
137 mandatory for document preparation. The legacy mode with implicit |
|
138 copying of the document/ directory is no longer supported. Minor |
|
139 INCOMPATIBILITY. |
135 |
140 |
136 |
141 |
137 *** Pure *** |
142 *** Pure *** |
138 |
143 |
139 * Proof methods with explicit instantiation ("rule_tac", "subgoal_tac" |
144 * Proof methods with explicit instantiation ("rule_tac", "subgoal_tac" |