equal
deleted
inserted
replaced
32 |
32 |
33 |
33 |
34 *** Pure *** |
34 *** Pure *** |
35 |
35 |
36 * More thorough check of proof context for goal statements and |
36 * More thorough check of proof context for goal statements and |
37 attributed fact expressions: background theory, declared hyps, |
37 attributed fact expressions (concerning background theory, declared |
38 declared variable names. Potential INCOMPATIBILITY, tools need to |
38 hyps). Potential INCOMPATIBILITY, tools need to observe standard |
39 observe standard context discipline. |
39 context discipline. See also Assumption.add_assumes and the more |
|
40 primitive Thm.assume_hyps. |
40 |
41 |
41 |
42 |
42 *** HOL *** |
43 *** HOL *** |
43 |
44 |
44 * "declare [[code abort: ...]]" replaces "code_abort ...". |
45 * "declare [[code abort: ...]]" replaces "code_abort ...". |