blanchet [Sun, 01 May 2011 18:37:24 +0200] rev 42534
fake type declarations for full-type args and mangled type encodings, so that type assumptions can be discharged
blanchet [Sun, 01 May 2011 18:37:24 +0200] rev 42533
generate TFF type declarations in typed mode
blanchet [Sun, 01 May 2011 18:37:24 +0200] rev 42532
no point in keeping indices in Sledgehammer readable var names, since these are disambiguated anyway
blanchet [Sun, 01 May 2011 18:37:24 +0200] rev 42531
added more rudimentary type support to Sledgehammer's ATP encoding
blanchet [Sun, 01 May 2011 18:37:24 +0200] rev 42530
fixed type of ATP quantifier types (sic)
blanchet [Sun, 01 May 2011 18:37:24 +0200] rev 42529
added "useful_info" argument to ATP formulas -- this will probably be useful later to specify intro, simp, elim to SPASS