equal
deleted
inserted
replaced
3 |
3 |
4 New in this Isabelle version |
4 New in this Isabelle version |
5 ---------------------------- |
5 ---------------------------- |
6 |
6 |
7 *** General *** |
7 *** General *** |
|
8 |
|
9 * Command 'experiment' opens an anonymous locale context with private |
|
10 naming policy. |
8 |
11 |
9 * Structural composition of proof methods (meth1; meth2) in Isar |
12 * Structural composition of proof methods (meth1; meth2) in Isar |
10 corresponds to (tac1 THEN_ALL_NEW tac2) in ML. |
13 corresponds to (tac1 THEN_ALL_NEW tac2) in ML. |
11 |
14 |
12 * Generated schematic variables in standard format of exported facts are |
15 * Generated schematic variables in standard format of exported facts are |