equal
deleted
inserted
replaced
16 |
16 |
17 defs rep_NP_def "rep_NP x == (case x of abs_NP y => y)" |
17 defs rep_NP_def "rep_NP x == (case x of abs_NP y => y)" |
18 |
18 |
19 (* NPAIR (continued) *) |
19 (* NPAIR (continued) *) |
20 defs per_NP_def |
20 defs per_NP_def |
21 "eqv ==(%x y.fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))" |
21 "eqv ==(%x y. fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))" |
22 |
22 |
23 (* for proves of this rule see [Slo97diss] *) |
23 (* for proves of this rule see [Slo97diss] *) |
24 rules |
24 rules |
25 per_trans_NP "[| eqv (x::NP) y;eqv y z |] ==> eqv x z" |
25 per_trans_NP "[| eqv (x::NP) y;eqv y z |] ==> eqv x z" |
26 end |
26 end |