equal
deleted
inserted
replaced
30 process, without requiring old-fashioned command-line invocation of |
30 process, without requiring old-fashioned command-line invocation of |
31 "isabelle jedit -m MODE". |
31 "isabelle jedit -m MODE". |
32 |
32 |
33 |
33 |
34 *** HOL *** |
34 *** HOL *** |
|
35 |
|
36 * "declare [[code abort: …]]" replaces "code_abort …". |
|
37 INCOMPATIBILITY. |
|
38 |
|
39 * "declare [[code drop: …]]" drops all code equations associated |
|
40 with the given constants. |
35 |
41 |
36 * Abolished slightly odd global lattice interpretation for min/max. |
42 * Abolished slightly odd global lattice interpretation for min/max. |
37 |
43 |
38 Fact consolidations: |
44 Fact consolidations: |
39 min_max.inf_assoc ~> min.assoc |
45 min_max.inf_assoc ~> min.assoc |