wneuper/isa: File revisions

src/HOL/SMT/Tools/z3_proof_tools.ML

Wed, 12 May 2010 23:54:00 +0200	use proper context operations (for fresh names of type and term variables, and for hypothetical definitions), monomorphize theorems (instead of terms, necessary for hypothetical definitions made during lambda lifting)	file \| diff \| annotate
Wed, 12 May 2010 23:53:59 +0200	split monolithic Z3 proof reconstruction structure into separate structures, use one set of schematic theorems for all uncertain proof rules (to extend proof reconstruction by missing cases), added several schematic theorems, improved abstraction of goals (abstract all uninterpreted sub-terms, only leave builtin symbols)	file \| diff \| annotate

wneuper/isa