| changeset 2692 | da9bed7baf23 |
| parent 2689 | ddc05a611005 |
| child 2695 | e8736c1cdd7f |
| 2691:abb6c3ac2df2 | 2692:da9bed7baf23 |
|---|---|
21 variables) and the typing judgement. |
21 variables) and the typing judgement. |
22 |
22 |
23 *} |
23 *} |
24 |
24 |
25 type_synonym ty_ctx = "(name \<times> ty) list" |
25 type_synonym ty_ctx = "(name \<times> ty) list" |
26 |
|
27 |
26 |
28 inductive |
27 inductive |
29 valid :: "ty_ctx \<Rightarrow> bool" |
28 valid :: "ty_ctx \<Rightarrow> bool" |
30 where |
29 where |
31 v1[intro]: "valid []" |
30 v1[intro]: "valid []" |