equal
deleted
inserted
replaced
57 Thy_Output.source thy_output_source |
57 Thy_Output.source thy_output_source |
58 Thy_Output.break thy_output_break |
58 Thy_Output.break thy_output_break |
59 |
59 |
60 Note that corresponding "..._default" references in ML may be only |
60 Note that corresponding "..._default" references in ML may be only |
61 changed globally at the ROOT session setup, but *not* within a theory. |
61 changed globally at the ROOT session setup, but *not* within a theory. |
|
62 |
|
63 * More systematic naming of some configuration options. |
|
64 INCOMPATIBILTY. |
|
65 |
|
66 trace_simp ~> simp_trace |
|
67 debug_simp ~> simp_debug |
62 |
68 |
63 |
69 |
64 *** Pure *** |
70 *** Pure *** |
65 |
71 |
66 * Support for real valued configuration options, using simplistic |
72 * Support for real valued configuration options, using simplistic |