equal
deleted
inserted
replaced
19 FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for |
19 FOL, ZF, ZFC etc. INCOMPATIBILITY, need to use qualified names for |
20 formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK". |
20 formerly global "HOL-Probability.Probability" and "HOL-SPARK.SPARK". |
21 |
21 |
22 * Global facts need to be closed: no free variables and no hypotheses. |
22 * Global facts need to be closed: no free variables and no hypotheses. |
23 Rare INCOMPATIBILITY. |
23 Rare INCOMPATIBILITY. |
|
24 |
|
25 * Facts stemming from locale interpretation are subject to lazy |
|
26 evaluation for improved performance. Rare INCOMPATIBILITY: errors |
|
27 stemming from interpretation morphisms might be deferred and thus |
|
28 difficult to locate; enable system option "strict_facts" temporarily to |
|
29 avoid this. |
24 |
30 |
25 * Marginal comments need to be written exclusively in the new-style form |
31 * Marginal comments need to be written exclusively in the new-style form |
26 "\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer |
32 "\<comment> \<open>text\<close>", old ASCII variants like "-- {* ... *}" are no longer |
27 supported. INCOMPATIBILITY, use the command-line tool "isabelle |
33 supported. INCOMPATIBILITY, use the command-line tool "isabelle |
28 update_comments" to update existing theory files. |
34 update_comments" to update existing theory files. |