2010-05-28 wenzelm [Fri, 28 May 2010 11:23:34 +0200] rev 37159
some updates for release;
ANNOUNCE COPYRIGHT README

2010-05-27 wenzelm [Thu, 27 May 2010 21:37:42 +0200] rev 37158
merged
NEWS

2010-05-27 boehmes [Thu, 27 May 2010 18:16:54 +0200] rev 37157
added function update examples and set examples
src/HOL/SMT.thy src/HOL/SMT_Examples/SMT_Tests.certs src/HOL/SMT_Examples/SMT_Tests.thy

2010-05-27 boehmes [Thu, 27 May 2010 17:09:37 +0200] rev 37156
updated SMT certificates
src/HOL/Boogie/Examples/Boogie_Dijkstra.certs src/HOL/Boogie/Examples/Boogie_Max.certs src/HOL/Boogie/Examples/VCC_Max.certs src/HOL/Multivariate_Analysis/Integration.certs src/HOL/SMT_Examples/SMT_Examples.certs src/HOL/SMT_Examples/SMT_Tests.certs src/HOL/SMT_Examples/SMT_Word_Examples.certs

2010-05-27 boehmes [Thu, 27 May 2010 17:09:06 +0200] rev 37155
sort signature in SMT-LIB output (improves sharing of SMT certificates: goals of the same logical structure are translated into equal SMT-LIB benchmarks)
src/HOL/Tools/SMT/smtlib_interface.ML

2010-05-27 boehmes [Thu, 27 May 2010 16:30:26 +0200] rev 37154
merged
NEWS

2010-05-27 boehmes [Thu, 27 May 2010 16:29:33 +0200] rev 37153
renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
src/HOL/Boogie/Examples/Boogie_Dijkstra.certs src/HOL/SMT.thy src/HOL/SMT_Examples/SMT_Examples.certs src/HOL/Tools/SMT/smt_normalize.ML src/HOL/Tools/SMT/z3_interface.ML src/HOL/Tools/SMT/z3_model.ML

2010-05-27 boehmes [Thu, 27 May 2010 14:58:45 +0200] rev 37152
made script executable
src/HOL/Tools/SMT/lib/scripts/remote_smt

2010-05-27 boehmes [Thu, 27 May 2010 14:55:53 +0200] rev 37151
use Z3's builtin support for div and mod
src/HOL/SMT.thy src/HOL/SMT_Examples/SMT_Examples.certs src/HOL/SMT_Examples/SMT_Examples.thy src/HOL/SMT_Examples/SMT_Tests.certs src/HOL/SMT_Examples/SMT_Tests.thy src/HOL/Tools/SMT/z3_interface.ML src/HOL/Tools/SMT/z3_proof_tools.ML

2010-05-27 boehmes [Thu, 27 May 2010 14:54:13 +0200] rev 37150
moved SMT into the HOL image
NEWS