huffman [Tue, 16 Nov 2010 13:37:17 -0800] rev 40589
add bind_bind rules for powerdomains
wenzelm [Wed, 17 Nov 2010 13:50:02 +0100] rev 40588
merged
haftmann [Wed, 17 Nov 2010 12:24:58 +0100] rev 40587
emerging Isar command interface
haftmann [Wed, 17 Nov 2010 11:38:47 +0100] rev 40586
fixed typo
haftmann [Wed, 17 Nov 2010 11:38:46 +0100] rev 40585
updated keywords
haftmann [Wed, 17 Nov 2010 11:27:48 +0100] rev 40584
ML signature interface
haftmann [Wed, 17 Nov 2010 11:26:39 +0100] rev 40583
stub for Isar command interface
haftmann [Wed, 17 Nov 2010 11:09:18 +0100] rev 40582
module for functorial mappers
wenzelm [Wed, 17 Nov 2010 13:39:30 +0100] rev 40581
merged
boehmes [Wed, 17 Nov 2010 09:22:23 +0100] rev 40580
require the b2i file ending in the boogie_open command (for consistency with the theory header)
boehmes [Wed, 17 Nov 2010 08:14:56 +0100] rev 40579
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)
boehmes [Wed, 17 Nov 2010 08:14:55 +0100] rev 40578
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
huffman [Tue, 16 Nov 2010 12:08:28 -0800] rev 40577
add lemmas about powerdomains
huffman [Tue, 16 Nov 2010 11:57:10 -0800] rev 40576
declare {upper,lower,convex}_pd_induct as default induction rules
huffman [Tue, 16 Nov 2010 11:50:05 -0800] rev 40575
rename 'repdef' to 'domaindef'
wenzelm [Wed, 17 Nov 2010 13:38:53 +0100] rev 40574
refrain from opening Scratch.thy by default, to avoid bombing the editor with old/long theory text;
wenzelm [Wed, 17 Nov 2010 11:24:07 +0100] rev 40573
less parentheses, cf. Session.welcome;
wenzelm [Tue, 16 Nov 2010 22:40:45 +0100] rev 40572
avoid spam;
wenzelm [Tue, 16 Nov 2010 22:13:54 +0100] rev 40571
more robust determination of java executable;
wenzelm [Tue, 16 Nov 2010 21:54:52 +0100] rev 40570
init_component: require absolute path (when invoked by user scripts);
wenzelm [Tue, 16 Nov 2010 21:48:14 +0100] rev 40569
more explicit explanation of init_component shell function;
wenzelm [Tue, 16 Nov 2010 20:30:25 +0100] rev 40568
paranoia export of CLASSPATH, just in case the initial status via allexport is lost due to other scripts;
wenzelm [Tue, 16 Nov 2010 17:27:11 +0100] rev 40567
tuned message;
wenzelm [Tue, 16 Nov 2010 15:29:01 +0100] rev 40566
post raw messages last, to ensure that result has been handled by session actor already (e.g. to avoid race between Session.session_actor and Session_Dockable.main_actor);
wenzelm [Tue, 16 Nov 2010 15:23:26 +0100] rev 40565
more reasonably defaults for typical laptops (2 GB RAM, 2 cores);
enforce -server JVM if possible (NB: default JRE on Windows lacks that);
haftmann [Tue, 16 Nov 2010 10:33:36 +0100] rev 40564
added forall2 predicate lifter
wenzelm [Mon, 15 Nov 2010 22:31:18 +0100] rev 40563
merged
boehmes [Mon, 15 Nov 2010 22:24:08 +0100] rev 40562
merged
boehmes [Mon, 15 Nov 2010 22:23:28 +0100] rev 40561
renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed
boehmes [Mon, 15 Nov 2010 22:23:26 +0100] rev 40560
honour timeouts which are not rounded to full seconds