equal
deleted
inserted
replaced
21 * Outer syntax commands are managed authentically within the theory |
21 * Outer syntax commands are managed authentically within the theory |
22 context, without implicit global state. Potential for accidental |
22 context, without implicit global state. Potential for accidental |
23 INCOMPATIBILITY, make sure that required theories are really imported. |
23 INCOMPATIBILITY, make sure that required theories are really imported. |
24 |
24 |
25 * 'find_theorems': search patterns which are abstractions are |
25 * 'find_theorems': search patterns which are abstractions are |
26 schematcially expanded before search. Search results match the naive |
26 schematically expanded before search. Search results match the naive |
27 expectation more closely, particularly wrt. abbreviations. |
27 expectation more closely, particularly wrt. abbreviations. |
28 INCOMPATIBILITY. |
28 INCOMPATIBILITY. |
29 |
29 |
30 |
30 |
31 *** Prover IDE -- Isabelle/Scala/jEdit *** |
31 *** Prover IDE -- Isabelle/Scala/jEdit *** |