isabelle: File revisions

src/HOL/Tools/SMT/verit_isar.ML

Tue, 13 Oct 2020 16:45:38 +0200	Mathias Fleury	reconstruction of veriT proofs in NEWS	file \| diff \| annotate
Mon, 12 Oct 2020 18:59:44 +0200	Mathias Fleury	add reconstruction for the SMT solver veriT	file \| diff \| annotate
Thu, 02 Oct 2014 17:39:38 +0200	blanchet	avoid duplicate 'obtain' in veriT Isar proofs, by removing dubious condition	file \| diff \| annotate
Tue, 30 Sep 2014 12:47:15 +0200	blanchet	repaired index confusion -- in particular, carefully distinguish between 'assert indices' (monomorphised etc.) and 'assume indices'	file \| diff \| annotate
Tue, 30 Sep 2014 11:06:26 +0200	blanchet	keep rules with no premises in Isar proofs from veriT	file \| diff \| annotate
Mon, 29 Sep 2014 18:37:33 +0200	blanchet	simplified and repaired veriT index handling code	file \| diff \| annotate
Thu, 28 Aug 2014 00:40:38 +0200	blanchet	keep skolems as is -- otherwise this breaks proof steps that refer to variables that were 'obtain'ed in the outer Isar proof	file \| diff \| annotate
Thu, 28 Aug 2014 00:40:38 +0200	blanchet	renamed new SMT module from 'SMT2' to 'SMT'	file \| diff \| annotate \| base

isabelle