equal
deleted
inserted
replaced
31 operating on the goal state. In any case, the standard discipline for |
31 operating on the goal state. In any case, the standard discipline for |
32 subgoal-addressing needs to be observed: no subgoals or a subgoal |
32 subgoal-addressing needs to be observed: no subgoals or a subgoal |
33 number that is out of range produces an empty result sequence, not an |
33 number that is out of range produces an empty result sequence, not an |
34 exception. Potential INCOMPATIBILITY for non-conformant tactical |
34 exception. Potential INCOMPATIBILITY for non-conformant tactical |
35 proof tools. |
35 proof tools. |
|
36 |
|
37 * Discontinued old Toplevel.debug in favour of system option |
|
38 "exception_trace", which may be also declared within the context via |
|
39 "declare [[exception_trace = true]]". Minor INCOMPATIBILITY. |
36 |
40 |
37 |
41 |
38 *** Prover IDE -- Isabelle/Scala/jEdit *** |
42 *** Prover IDE -- Isabelle/Scala/jEdit *** |
39 |
43 |
40 * Auxiliary files ('ML_file' etc.) are managed by the Prover IDE. |
44 * Auxiliary files ('ML_file' etc.) are managed by the Prover IDE. |