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 * Local theory specifications may have a 'private' modifier to restrict |
|
10 name space accesses to the current local scope, as delimited by "context |
|
11 begin ... end". For example, this works like this: |
|
12 |
|
13 context |
|
14 begin |
|
15 |
|
16 private definition ... |
|
17 private definition ... |
|
18 private lemma ... |
|
19 |
|
20 lemma ... |
|
21 lemma ... |
|
22 theorem ... |
|
23 |
|
24 end |
8 |
25 |
9 * Command 'experiment' opens an anonymous locale context with private |
26 * Command 'experiment' opens an anonymous locale context with private |
10 naming policy. |
27 naming policy. |
11 |
28 |
12 * Structural composition of proof methods (meth1; meth2) in Isar |
29 * Structural composition of proof methods (meth1; meth2) in Isar |