renamed 'defns' to 'defs';
removed 'sigclass';
replaced parents by enclose;
exported parens, brackets, mk_list, mk_big_list, mk_pair, mk_triple;
various minor internal changes;
FOLP = IFOLP +
consts
cla :: "[p=>p]=>p"
rules
classical "(!!x.x:~P ==> f(x):P) ==> cla(f):P"
end