src/HOL/Tools/SMT/z3_proof_methods.ML
2011-11-07 boehmes 2011-11-07 replace higher-order matching against schematic theorem with dedicated reconstruction method
2011-10-25 boehmes 2011-10-25 clarify types of terms: use proper set type
2011-03-09 boehmes 2011-03-09 finished and tested Z3 proof reconstruction for injective functions; only treat variables as atomic, and especially abstract constants (Isabelle's interpretation of these constants is most likely not known to Z3 and thus irrelevant for the proof)
2010-12-20 boehmes 2010-12-20 avoid ML structure aliases (especially single-letter abbreviations)
2010-12-01 wenzelm 2010-12-01 just one Term.dest_funT;
2010-11-22 boehmes 2010-11-22 share and use more utility functions; slightly reduced complexity for Z3 proof rule 'rewrite'
2010-11-22 boehmes 2010-11-22 added prove reconstruction for injective functions; added SMT_Utils to collect frequently used functions