equal
deleted
inserted
replaced
|
1 theory Implementation |
|
2 imports PIPBasics |
|
3 begin |
|
4 |
1 section {* |
5 section {* |
2 This file contains lemmas used to guide the recalculation of current precedence |
6 This file contains lemmas used to guide the recalculation of current precedence |
3 after every system call (or system operation) |
7 after every system call (or system operation) |
4 *} |
8 *} |
5 theory Implementation |
|
6 imports PIPBasics |
|
7 begin |
|
8 |
9 |
9 text {* (* ddd *) |
10 text {* (* ddd *) |
10 One beauty of our modelling is that we follow the definitional extension tradition of HOL. |
11 One beauty of our modelling is that we follow the definitional extension tradition of HOL. |
11 The benefit of such a concise and miniature model is that large number of intuitively |
12 The benefit of such a concise and miniature model is that large number of intuitively |
12 obvious facts are derived as lemmas, rather than asserted as axioms. |
13 obvious facts are derived as lemmas, rather than asserted as axioms. |