equal
deleted
inserted
replaced
12 * Updated and extended "isar-ref" manual, reduced remaining material |
12 * Updated and extended "isar-ref" manual, reduced remaining material |
13 in old "ref" manual. |
13 in old "ref" manual. |
14 |
14 |
15 |
15 |
16 *** Pure *** |
16 *** Pure *** |
|
17 |
|
18 * Command "export_code": relative file names are interpreted |
|
19 relatively to master directory of current theory rather than |
|
20 the rather arbitrary current working directory. |
|
21 INCOMPATIBILITY. |
17 |
22 |
18 * Discontinued obsolete attribute "COMP". Potential INCOMPATIBILITY, |
23 * Discontinued obsolete attribute "COMP". Potential INCOMPATIBILITY, |
19 use regular rule composition via "OF" / "THEN", or explicit proof |
24 use regular rule composition via "OF" / "THEN", or explicit proof |
20 structure instead. Note that Isabelle/ML provides a variety of |
25 structure instead. Note that Isabelle/ML provides a variety of |
21 operators like COMP, INCR_COMP, COMP_INCR, which need to be applied |
26 operators like COMP, INCR_COMP, COMP_INCR, which need to be applied |