equal
deleted
inserted
replaced
8 |
8 |
9 FOLP = IFOLP + |
9 FOLP = IFOLP + |
10 consts |
10 consts |
11 cla :: "[p=>p]=>p" |
11 cla :: "[p=>p]=>p" |
12 rules |
12 rules |
13 classical "(!!x.x:~P ==> f(x):P) ==> cla(f):P" |
13 classical "(!!x. x:~P ==> f(x):P) ==> cla(f):P" |
14 end |
14 end |