| changeset 68776 | 403dd13cf6e9 |
| parent 67406 | 23307fd33906 |
| child 69505 | cc2d676d5395 |
| 68774:9fc50a3e07f6 | 68776:403dd13cf6e9 |
|---|---|
1 section "Security Type Systems" |
1 section "Security Type Systems" |
2 |
|
3 subsection "Security Levels and Expressions" |
|
2 |
4 |
3 theory Sec_Type_Expr imports Big_Step |
5 theory Sec_Type_Expr imports Big_Step |
4 begin |
6 begin |
5 |
|
6 subsection "Security Levels and Expressions" |
|
7 |
7 |
8 type_synonym level = nat |
8 type_synonym level = nat |
9 |
9 |
10 class sec = |
10 class sec = |
11 fixes sec :: "'a \<Rightarrow> nat" |
11 fixes sec :: "'a \<Rightarrow> nat" |