20111107 
boehmes 
20111107 
replace higherorder matching against schematic theorem with dedicated reconstruction method

file  diff  annotate 
20111025 
boehmes 
20111025 
clarify types of terms: use proper set type

file  diff  annotate 
20110309 
boehmes 
20110309 
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)

file  diff  annotate 
20101220 
boehmes 
20101220 
avoid ML structure aliases (especially singleletter abbreviations)

file  diff  annotate 
20101201 
wenzelm 
20101201 
just one Term.dest_funT;

file  diff  annotate 
20101122 
boehmes 
20101122 
share and use more utility functions;
slightly reduced complexity for Z3 proof rule 'rewrite'

file  diff  annotate 
20101122 
boehmes 
20101122 
added prove reconstruction for injective functions;
added SMT_Utils to collect frequently used functions

file  diff  annotate 