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. |
|
40 |
36 |
41 * Command 'SML_file' reads and evaluates the given Standard ML file. |
37 * Command 'SML_file' reads and evaluates the given Standard ML file. |
42 Toplevel bindings are stored within the theory context; the initial |
38 Toplevel bindings are stored within the theory context; the initial |
43 environment is restricted to the Standard ML implementation of |
39 environment is restricted to the Standard ML implementation of |
44 Poly/ML, without the add-ons of Isabelle/ML. See also |
40 Poly/ML, without the add-ons of Isabelle/ML. See also |
542 specific and may override results accumulated so far. The elements |
538 specific and may override results accumulated so far. The elements |
543 guard is mandatory and checked precisely. Subtle INCOMPATIBILITY. |
539 guard is mandatory and checked precisely. Subtle INCOMPATIBILITY. |
544 |
540 |
545 |
541 |
546 *** ML *** |
542 *** ML *** |
|
543 |
|
544 * Discontinued old Toplevel.debug in favour of system option |
|
545 "ML_exception_trace", which may be also declared within the context via |
|
546 "declare [[ML_exception_trace = true]]". Minor INCOMPATIBILITY. |
|
547 |
|
548 * Renamed option "ML_trace" to "ML_source_trace". Minor |
|
549 INCOMPATIBILITY. |
547 |
550 |
548 * Proper context discipline for read_instantiate and instantiate_tac: |
551 * Proper context discipline for read_instantiate and instantiate_tac: |
549 variables that are meant to become schematic need to be given as |
552 variables that are meant to become schematic need to be given as |
550 fixed, and are generalized by the explicit context of local variables. |
553 fixed, and are generalized by the explicit context of local variables. |
551 This corresponds to Isar attributes "where" and "of" with 'for' |
554 This corresponds to Isar attributes "where" and "of" with 'for' |