haftmann [Thu, 18 Nov 2010 17:01:15 +0100] rev 40602
map_fun combinator in theory Fun
wenzelm [Thu, 18 Nov 2010 22:34:32 +0100] rev 40601
some updates after 2 years of Mercurial usage;
blanchet [Thu, 18 Nov 2010 18:12:03 +0100] rev 40600
mention Sledgehammer with SMT
blanchet [Thu, 18 Nov 2010 18:09:08 +0100] rev 40599
enabled SMT solver in Sledgehammer by default
haftmann [Thu, 18 Nov 2010 12:37:30 +0100] rev 40598
merged
haftmann [Thu, 18 Nov 2010 10:59:42 +0100] rev 40597
keep variables bound
blanchet [Thu, 18 Nov 2010 10:52:38 +0100] rev 40596
remove "Time limit reached" as potential error, because this is sometimes generated for individual slices and not for the entire problem
haftmann [Wed, 17 Nov 2010 23:20:26 +0100] rev 40595
merged
haftmann [Wed, 17 Nov 2010 17:27:25 +0100] rev 40594
infer variances of user-given mapper operation; proper thm storing
nipkow [Wed, 17 Nov 2010 21:35:23 +0100] rev 40593
code eqn for slice was missing; redefined splice with fun
huffman [Wed, 17 Nov 2010 08:47:58 -0800] rev 40592
move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman [Wed, 17 Nov 2010 06:49:23 -0800] rev 40591
merged
huffman [Tue, 16 Nov 2010 16:36:57 -0800] rev 40590
typedef (open) unit
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;