2010-11-12 turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
boehmes [Fri, 12 Nov 2010 15:56:10 +0100] rev 40515
turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user
2010-11-12 let the theory formally depend on the Boogie output
boehmes [Fri, 12 Nov 2010 15:56:08 +0100] rev 40514
let the theory formally depend on the Boogie output
2010-11-12 look for certificates relative to the theory
boehmes [Fri, 12 Nov 2010 15:56:07 +0100] rev 40513
look for certificates relative to the theory
2010-11-12 dropped numerals from monomorphization blacklist (only particular numerals are builtin, all other numerals should be treated uninterpreted), this blacklist should contain only truely polymorphic builtin constants supported by SMT
boehmes [Fri, 12 Nov 2010 15:56:06 +0100] rev 40512
dropped numerals from monomorphization blacklist (only particular numerals are builtin, all other numerals should be treated uninterpreted), this blacklist should contain only truely polymorphic builtin constants supported by SMT
2010-11-12 merged
huffman [Fri, 12 Nov 2010 06:11:29 -0800] rev 40511
merged
2010-11-12 update Theory.requires with new theory name
huffman [Fri, 12 Nov 2010 06:05:26 -0800] rev 40510
update Theory.requires with new theory name
2010-11-12 tuned signatures;
wenzelm [Fri, 12 Nov 2010 14:51:28 +0100] rev 40509
tuned signatures;
2010-11-12 never open Unsynchronized;
wenzelm [Fri, 12 Nov 2010 14:06:37 +0100] rev 40508
never open Unsynchronized;
2010-11-12 merged
wenzelm [Fri, 12 Nov 2010 12:57:02 +0100] rev 40507
merged
2010-11-11 section headings
huffman [Wed, 10 Nov 2010 18:45:48 -0800] rev 40506
section headings
2010-11-11 reorder chapters for generated document
huffman [Wed, 10 Nov 2010 18:37:11 -0800] rev 40505
reorder chapters for generated document
2010-11-11 merge Representable.thy into Domain.thy
huffman [Wed, 10 Nov 2010 18:30:17 -0800] rev 40504
merge Representable.thy into Domain.thy
2010-11-11 move stuff from Domain.thy to Domain_Aux.thy
huffman [Wed, 10 Nov 2010 18:15:21 -0800] rev 40503
move stuff from Domain.thy to Domain_Aux.thy
2010-11-11 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman [Wed, 10 Nov 2010 17:56:08 -0800] rev 40502
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
2010-11-10 allow unpointed lazy arguments for definitional domain package
huffman [Wed, 10 Nov 2010 14:59:52 -0800] rev 40501
allow unpointed lazy arguments for definitional domain package
2010-11-10 add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman [Wed, 10 Nov 2010 14:20:47 -0800] rev 40500
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
2010-11-10 merged
huffman [Wed, 10 Nov 2010 13:22:39 -0800] rev 40499
merged
2010-11-10 removed unused lemma chain_mono2
huffman [Wed, 10 Nov 2010 13:08:42 -0800] rev 40498
removed unused lemma chain_mono2
2010-11-10 rename class 'bifinite' to 'domain'
huffman [Wed, 10 Nov 2010 11:42:35 -0800] rev 40497
rename class 'bifinite' to 'domain'
2010-11-10 instance sum :: (predomain, predomain) predomain
huffman [Wed, 10 Nov 2010 09:59:08 -0800] rev 40496
instance sum :: (predomain, predomain) predomain
2010-11-10 configure sum type for fixrec
huffman [Wed, 10 Nov 2010 09:52:50 -0800] rev 40495
configure sum type for fixrec
2010-11-10 add class liftdomain, for bifinite domains where DEFL('a u) = u_defl('a)
huffman [Wed, 10 Nov 2010 08:18:32 -0800] rev 40494
add class liftdomain, for bifinite domains where DEFL('a u) = u_defl('a)
2010-11-10 instance prod :: (predomain, predomain) predomain
huffman [Wed, 10 Nov 2010 06:02:37 -0800] rev 40493
instance prod :: (predomain, predomain) predomain
2010-11-10 adapt isodefl proof script to unpointed types
huffman [Tue, 09 Nov 2010 19:37:11 -0800] rev 40492
adapt isodefl proof script to unpointed types
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -24 +24 +50 +100 +300 +1000 +3000 +10000 +30000 tip