equal
deleted
inserted
replaced
39 context discipline. See also Assumption.add_assumes and the more |
39 context discipline. See also Assumption.add_assumes and the more |
40 primitive Thm.assume_hyps. |
40 primitive Thm.assume_hyps. |
41 |
41 |
42 |
42 |
43 *** HOL *** |
43 *** HOL *** |
|
44 |
|
45 * Activation of Z3 now works via "z3_non_commercial" system option |
|
46 (without requiring restart), instead of former settings variable |
|
47 "Z3_NON_COMMERCIAL". The option can be edited in Isabelle/jEdit menu |
|
48 Plugin Options / Isabelle / General. |
44 |
49 |
45 * "declare [[code abort: ...]]" replaces "code_abort ...". |
50 * "declare [[code abort: ...]]" replaces "code_abort ...". |
46 INCOMPATIBILITY. |
51 INCOMPATIBILITY. |
47 |
52 |
48 * "declare [[code drop: ...]]" drops all code equations associated |
53 * "declare [[code drop: ...]]" drops all code equations associated |