equal
deleted
inserted
replaced
85 trans "[| $H|- $E, a=b, $F; $H|- $E, b=c, $F |] ==> $H|- $E, a=c, $F" |
85 trans "[| $H|- $E, a=b, $F; $H|- $E, b=c, $F |] ==> $H|- $E, a=c, $F" |
86 |
86 |
87 |
87 |
88 (*Descriptions*) |
88 (*Descriptions*) |
89 |
89 |
90 The "[| $H |- $E, P(a), $F; !!x.$H, P(x) |- $E, x=a, $F |] ==> \ |
90 The "[| $H |- $E, P(a), $F; !!x.$H, P(x) |- $E, x=a, $F |] ==> |
91 \ $H |- $E, P(THE x.P(x)), $F" |
91 $H |- $E, P(THE x.P(x)), $F" |
92 end |
92 end |
93 |
93 |
94 ML |
94 ML |
95 |
95 |
96 (*Abstract over "sobj" -- representation of a sequence of formulae *) |
96 (*Abstract over "sobj" -- representation of a sequence of formulae *) |