changeset 71 | 729fe026c5f3 |
parent 16 | 0b033d50ca1c |
child 419 | 7c7e71be40c8 |
70:8a29f8b4aca1 | 71:729fe026c5f3 |
---|---|
22 val sintrs = |
22 val sintrs = |
23 ["Fls : prop", |
23 ["Fls : prop", |
24 "n: nat ==> #n : prop", |
24 "n: nat ==> #n : prop", |
25 "[| p: prop; q: prop |] ==> p=>q : prop"]; |
25 "[| p: prop; q: prop |] ==> p=>q : prop"]; |
26 val monos = []; |
26 val monos = []; |
27 val type_intrs = data_typechecks; |
27 val type_intrs = datatype_intrs; |
28 val type_elims = []); |
28 val type_elims = []); |
29 |
29 |
30 val [FlsI,VarI,ImpI] = Prop.intrs; |
30 val [FlsI,VarI,ImpI] = Prop.intrs; |
31 |
31 |
32 |
32 |