isabelle: File revisions

src/HOL/Tools/SMT/z3_proof_literals.ML

Wed, 15 Feb 2012 23:19:30 +0100	wenzelm	renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;	file \| diff \| annotate
Mon, 12 Sep 2011 07:55:43 +0200	nipkow	new fastforce replacing fastsimp - less confusing name	file \| diff \| annotate
Mon, 20 Dec 2010 22:02:57 +0100	boehmes	avoid ML structure aliases (especially single-letter abbreviations)	file \| diff \| annotate
Wed, 15 Dec 2010 16:29:56 +0100	boehmes	the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils	file \| diff \| annotate
Wed, 15 Dec 2010 08:39:24 +0100	boehmes	tuned	file \| diff \| annotate
Wed, 17 Nov 2010 08:14:56 +0100	boehmes	use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable)	file \| diff \| annotate
Sat, 28 Aug 2010 16:14:32 +0200	haftmann	formerly unnamed infix equality now named HOL.eq	file \| diff \| annotate
Fri, 27 Aug 2010 10:56:46 +0200	haftmann	formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj	file \| diff \| annotate
Wed, 12 May 2010 23:54:02 +0200	boehmes	integrated SMT into the HOL image	file \| diff \| annotate

isabelle