blanchet [Sun, 17 Jul 2011 14:12:45 +0200] rev 44734
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
blanchet [Sun, 17 Jul 2011 14:11:35 +0200] rev 44733
pass kind to lambda-translation function
blanchet [Sun, 17 Jul 2011 14:11:35 +0200] rev 44732
more refactoring of preprocessing
blanchet [Sun, 17 Jul 2011 14:11:35 +0200] rev 44731
more refactoring of preprocessing, so as to be able to centralize it
blanchet [Sun, 17 Jul 2011 14:11:35 +0200] rev 44730
renamed internal data structure
blanchet [Sun, 17 Jul 2011 14:11:35 +0200] rev 44729
simplify code -- there are no lambdas in helpers anyway
blanchet [Sun, 17 Jul 2011 14:11:35 +0200] rev 44728
added lambda-lifting to Sledgehammer (rough)
blanchet [Sun, 17 Jul 2011 14:11:34 +0200] rev 44727
move more lambda-handling logic to Sledgehammer, from ATP module, for formal dependency reasons
haftmann [Sun, 17 Jul 2011 08:45:06 +0200] rev 44726
merged
haftmann [Sat, 16 Jul 2011 22:28:35 +0200] rev 44725
generalized some lemmas