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