equal
deleted
inserted
replaced
35 subgoal-addressing needs to be observed: no subgoals or a subgoal |
35 subgoal-addressing needs to be observed: no subgoals or a subgoal |
36 number that is out of range produces an empty result sequence, not an |
36 number that is out of range produces an empty result sequence, not an |
37 exception. Potential INCOMPATIBILITY for non-conformant tactical |
37 exception. Potential INCOMPATIBILITY for non-conformant tactical |
38 proof tools. |
38 proof tools. |
39 |
39 |
40 * Command 'SML_file' reads and evaluates the given Standard ML file. |
40 * Support for official Standard ML within the Isabelle context. |
|
41 Command 'SML_file' reads and evaluates the given Standard ML file. |
41 Toplevel bindings are stored within the theory context; the initial |
42 Toplevel bindings are stored within the theory context; the initial |
42 environment is restricted to the Standard ML implementation of |
43 environment is restricted to the Standard ML implementation of |
43 Poly/ML, without the add-ons of Isabelle/ML. See also |
44 Poly/ML, without the add-ons of Isabelle/ML. Commands 'SML_import' |
44 ~~/src/Tools/SML/Examples.thy for some basic examples. |
45 and 'SML_export' allow to exchange toplevel bindings between the two |
|
46 separate environments. See also ~~/src/Tools/SML/Examples.thy for |
|
47 some examples. |
45 |
48 |
46 |
49 |
47 *** Prover IDE -- Isabelle/Scala/jEdit *** |
50 *** Prover IDE -- Isabelle/Scala/jEdit *** |
48 |
51 |
49 * Improved syntactic and semantic completion mechanism: |
52 * Improved syntactic and semantic completion mechanism: |