equal
deleted
inserted
replaced
12 |
12 |
13 typedecl "term" |
13 typedecl "term" |
14 typedecl "context" |
14 typedecl "context" |
15 typedecl typing |
15 typedecl typing |
16 |
16 |
17 nonterminals |
17 nonterminal context' and typing' |
18 context' typing' |
|
19 |
18 |
20 consts |
19 consts |
21 Abs :: "[term, term => term] => term" |
20 Abs :: "[term, term => term] => term" |
22 Prod :: "[term, term => term] => term" |
21 Prod :: "[term, term => term] => term" |
23 Trueprop :: "[context, typing] => prop" |
22 Trueprop :: "[context, typing] => prop" |