wenzelm [Sat, 13 Nov 2010 20:13:35 +0100] rev 40528
report malformed symbols;
wenzelm [Sat, 13 Nov 2010 20:06:52 +0100] rev 40527
qualified Symbol_Pos.symbol;
wenzelm [Sat, 13 Nov 2010 19:55:45 +0100] rev 40526
total Symbol.source;
wenzelm [Sat, 13 Nov 2010 19:47:23 +0100] rev 40525
eliminated slightly odd pervasive Symbol_Pos.symbol;
wenzelm [Sat, 13 Nov 2010 19:27:41 +0100] rev 40524
treat Unicode "replacement character" (i.e. decoding error) is malformed;
wenzelm [Sat, 13 Nov 2010 19:21:53 +0100] rev 40523
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
allow malformed symbols inside quoted material, comments etc. -- for improved user experience with incremental re-parsing;
refined treatment of malformed surrogates (Scala);
wenzelm [Sat, 13 Nov 2010 16:46:00 +0100] rev 40522
tuned;
wenzelm [Sat, 13 Nov 2010 12:32:21 +0100] rev 40521
back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;
wenzelm [Sat, 13 Nov 2010 11:41:02 +0100] rev 40520
await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;
wenzelm [Sat, 13 Nov 2010 00:24:41 +0100] rev 40519
updated README;
wenzelm [Fri, 12 Nov 2010 21:37:01 +0100] rev 40518
defensive defaults for more robust experience for new users;
wenzelm [Fri, 12 Nov 2010 17:44:03 +0100] rev 40517
merged
boehmes [Fri, 12 Nov 2010 15:56:11 +0100] rev 40516
preliminary support for newer versions of Z3
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
boehmes [Fri, 12 Nov 2010 15:56:08 +0100] rev 40514
let the theory formally depend on the Boogie output
boehmes [Fri, 12 Nov 2010 15:56:07 +0100] rev 40513
look for certificates relative to the theory
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
huffman [Fri, 12 Nov 2010 06:11:29 -0800] rev 40511
merged
huffman [Fri, 12 Nov 2010 06:05:26 -0800] rev 40510
update Theory.requires with new theory name
wenzelm [Fri, 12 Nov 2010 14:51:28 +0100] rev 40509
tuned signatures;
wenzelm [Fri, 12 Nov 2010 14:06:37 +0100] rev 40508
never open Unsynchronized;
wenzelm [Fri, 12 Nov 2010 12:57:02 +0100] rev 40507
merged
huffman [Wed, 10 Nov 2010 18:45:48 -0800] rev 40506
section headings
huffman [Wed, 10 Nov 2010 18:37:11 -0800] rev 40505
reorder chapters for generated document
huffman [Wed, 10 Nov 2010 18:30:17 -0800] rev 40504
merge Representable.thy into Domain.thy
huffman [Wed, 10 Nov 2010 18:15:21 -0800] rev 40503
move stuff from Domain.thy to Domain_Aux.thy
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
huffman [Wed, 10 Nov 2010 14:59:52 -0800] rev 40501
allow unpointed lazy arguments for definitional domain package
huffman [Wed, 10 Nov 2010 14:20:47 -0800] rev 40500
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
huffman [Wed, 10 Nov 2010 13:22:39 -0800] rev 40499
merged
huffman [Wed, 10 Nov 2010 13:08:42 -0800] rev 40498
removed unused lemma chain_mono2
huffman [Wed, 10 Nov 2010 11:42:35 -0800] rev 40497
rename class 'bifinite' to 'domain'