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