isabelle: File revisions

src/HOL/Tools/Sledgehammer/metis_reconstruct.ML

Thu, 30 Sep 2010 19:15:47 +0200	blanchet	reintroduced code that keeps track of whether the Isabelle and Metis proofs are in sync -- generalized to work with the new skolemizer	file \| diff \| annotate
Thu, 30 Sep 2010 00:29:37 +0200	blanchet	move functions closer to where they're used	file \| diff \| annotate
Wed, 29 Sep 2010 23:06:02 +0200	blanchet	second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions	file \| diff \| annotate
Wed, 29 Sep 2010 22:23:27 +0200	blanchet	first step towards a new skolemizer that doesn't require "Eps"	file \| diff \| annotate
Mon, 20 Sep 2010 11:51:19 +0200	blanchet	merge tracing of two related modules	file \| diff \| annotate
Fri, 17 Sep 2010 00:35:19 +0200	blanchet	make "subst_translation" more robust w.r.t. type instantiations like {_1234 \|-> 'a}	file \| diff \| annotate
Thu, 16 Sep 2010 17:30:29 +0200	blanchet	complete refactoring of Metis along the lines of Sledgehammer	file \| diff \| annotate
Thu, 16 Sep 2010 16:24:23 +0200	blanchet	added new "Metis_Reconstruct" module, temporarily empty	file \| diff \| annotate

isabelle