equal
deleted
inserted
replaced
4 New in this Isabelle version |
4 New in this Isabelle version |
5 ---------------------------- |
5 ---------------------------- |
6 |
6 |
7 *** General *** |
7 *** General *** |
8 |
8 |
9 * Local theory specifications may have a 'private' modifier to restrict |
9 * Local theory specification commands may have a 'private' or |
10 name space accesses to the current local scope, as delimited by "context |
10 'restricted' modifier to limit name space accesses to the local scope, |
11 begin ... end". For example, this works like this: |
11 as provided by some "context begin ... end" block. For example: |
12 |
12 |
13 context |
13 context |
14 begin |
14 begin |
15 |
15 |
16 private definition ... |
16 private definition ... |