equal
deleted
inserted
replaced
120 (*Descriptions*) |
120 (*Descriptions*) |
121 |
121 |
122 The: "[| $H |- $E, P(a), $F; !!x.$H, P(x) |- $E, x=a, $F |] ==> |
122 The: "[| $H |- $E, P(a), $F; !!x.$H, P(x) |- $E, x=a, $F |] ==> |
123 $H |- $E, P(THE x. P(x)), $F" |
123 $H |- $E, P(THE x. P(x)), $F" |
124 |
124 |
125 constdefs |
125 definition If :: "[o, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) where |
126 If :: "[o, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) |
|
127 "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)" |
126 "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)" |
128 |
127 |
129 |
128 |
130 (** Structural Rules on formulas **) |
129 (** Structural Rules on formulas **) |
131 |
130 |