boehmes [Thu, 27 May 2010 17:09:37 +0200] rev 37156
updated SMT certificates
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)
boehmes [Thu, 27 May 2010 16:30:26 +0200] rev 37154
merged
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")
boehmes [Thu, 27 May 2010 14:58:45 +0200] rev 37152
made script executable
boehmes [Thu, 27 May 2010 14:55:53 +0200] rev 37151
use Z3's builtin support for div and mod
boehmes [Thu, 27 May 2010 14:54:13 +0200] rev 37150
moved SMT into the HOL image
wenzelm [Thu, 27 May 2010 21:36:38 +0200] rev 37149
slightly odd workaround to ignore markup that is typically displaced;
wenzelm [Thu, 27 May 2010 21:14:53 +0200] rev 37148
substantial performance improvement by avoiding "re-ified" execution structure via future dependencies, instead use singleton execution (dummy future) that forces lazy state updates bottom-up;
tuned;
wenzelm [Thu, 27 May 2010 20:15:36 +0200] rev 37147
further formal thread-safety (follow-up to 88300168baf8) -- in practice there is only a single Isar toplevel loop, but this is not enforced;