equal
deleted
inserted
replaced
40 https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/net/doc-files/net-properties.html |
40 https://docs.oracle.com/en/java/javase/11/docs/api/java.base/java/net/doc-files/net-properties.html |
41 |
41 |
42 * More symbol definitions for the Z Notation (Isabelle fonts and LaTeX). |
42 * More symbol definitions for the Z Notation (Isabelle fonts and LaTeX). |
43 See also the group "Z Notation" in the Symbols dockable of |
43 See also the group "Z Notation" in the Symbols dockable of |
44 Isabelle/jEdit. |
44 Isabelle/jEdit. |
|
45 |
|
46 |
|
47 *** Isar *** |
|
48 |
|
49 * The improper proof command 'guess' is no longer part of by Pure, but |
|
50 provided by the separate theory "Pure-ex.Guess". INCOMPATIBILITY, |
|
51 existing applications need to import session "Pure-ex" and theory |
|
52 "Pure-ex.Guess". Afterwards it is usually better eliminate the 'guess' |
|
53 command, using explicit 'obtain' instead. |
45 |
54 |
46 |
55 |
47 *** Isabelle/jEdit Prover IDE *** |
56 *** Isabelle/jEdit Prover IDE *** |
48 |
57 |
49 * More robust 'proof' outline for method "induct": support nested cases. |
58 * More robust 'proof' outline for method "induct": support nested cases. |