| Mon, 15 Nov 2010 14:59:21 +0100 |
haftmann |
re-generalized type of option_rel and sum_rel (accident from 2989f9f3aa10)
|
changeset |
files
|
| Mon, 15 Nov 2010 14:14:38 +0100 |
haftmann |
re-generalized type of prod_rel (accident from 2989f9f3aa10)
|
changeset |
files
|
| Mon, 15 Nov 2010 00:20:36 +0100 |
boehmes |
formal dependency on b2i files
|
changeset |
files
|
| Sun, 14 Nov 2010 23:55:25 +0100 |
boehmes |
merged
|
changeset |
files
|
| Fri, 12 Nov 2010 17:28:43 +0100 |
boehmes |
check the return code of the SMT solver and raise an exception if the prover failed
|
changeset |
files
|
| Sun, 14 Nov 2010 17:33:28 +0100 |
wenzelm |
updated README;
|
changeset |
files
|
| Sun, 14 Nov 2010 15:25:01 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 14 Nov 2010 15:21:49 +0100 |
wenzelm |
cover 'write' as primitive proof command;
|
changeset |
files
|
| Sun, 14 Nov 2010 14:05:08 +0100 |
wenzelm |
clarified interact/print state: proof commands are treated as in TTY mode to get full response;
|
changeset |
files
|
| Sat, 13 Nov 2010 22:33:07 +0100 |
wenzelm |
somewhat adhoc replacement for 'thus' and 'hence';
|
changeset |
files
|
| Sat, 13 Nov 2010 21:46:24 +0100 |
wenzelm |
always print state of proof commands (notably "qed" etc.);
|
changeset |
files
|
| Sat, 13 Nov 2010 21:01:03 +0100 |
wenzelm |
simplified message: malformed symbols are fully internalized, i.e. can be printed without crashing;
|
changeset |
files
|
| Sat, 13 Nov 2010 20:49:02 +0100 |
wenzelm |
tuned message;
|
changeset |
files
|
| Sat, 13 Nov 2010 20:20:05 +0100 |
wenzelm |
proper escape in regex;
|
changeset |
files
|
| Sat, 13 Nov 2010 20:13:35 +0100 |
wenzelm |
report malformed symbols;
|
changeset |
files
|
| Sat, 13 Nov 2010 20:06:52 +0100 |
wenzelm |
qualified Symbol_Pos.symbol;
|
changeset |
files
|
| Sat, 13 Nov 2010 19:55:45 +0100 |
wenzelm |
total Symbol.source;
|
changeset |
files
|
| Sat, 13 Nov 2010 19:47:23 +0100 |
wenzelm |
eliminated slightly odd pervasive Symbol_Pos.symbol;
|
changeset |
files
|
| Sat, 13 Nov 2010 19:27:41 +0100 |
wenzelm |
treat Unicode "replacement character" (i.e. decoding error) is malformed;
|
changeset |
files
|
| Sat, 13 Nov 2010 19:21:53 +0100 |
wenzelm |
simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.);
|
changeset |
files
|
| Sat, 13 Nov 2010 16:46:00 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 13 Nov 2010 12:32:21 +0100 |
wenzelm |
back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;
|
changeset |
files
|
| Sat, 13 Nov 2010 11:41:02 +0100 |
wenzelm |
await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;
|
changeset |
files
|
| Sat, 13 Nov 2010 00:24:41 +0100 |
wenzelm |
updated README;
|
changeset |
files
|
| Fri, 12 Nov 2010 21:37:01 +0100 |
wenzelm |
defensive defaults for more robust experience for new users;
|
changeset |
files
|
| Fri, 12 Nov 2010 17:44:03 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 12 Nov 2010 15:56:11 +0100 |
boehmes |
preliminary support for newer versions of Z3
|
changeset |
files
|
| Fri, 12 Nov 2010 15:56:10 +0100 |
boehmes |
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
|
changeset |
files
|
| Fri, 12 Nov 2010 15:56:08 +0100 |
boehmes |
let the theory formally depend on the Boogie output
|
changeset |
files
|
| Fri, 12 Nov 2010 15:56:07 +0100 |
boehmes |
look for certificates relative to the theory
|
changeset |
files
|
| Fri, 12 Nov 2010 15:56:06 +0100 |
boehmes |
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
|
changeset |
files
|
| Fri, 12 Nov 2010 06:11:29 -0800 |
huffman |
merged
|
changeset |
files
|
| Fri, 12 Nov 2010 06:05:26 -0800 |
huffman |
update Theory.requires with new theory name
|
changeset |
files
|
| Fri, 12 Nov 2010 14:51:28 +0100 |
wenzelm |
tuned signatures;
|
changeset |
files
|
| Fri, 12 Nov 2010 14:06:37 +0100 |
wenzelm |
never open Unsynchronized;
|
changeset |
files
|
| Fri, 12 Nov 2010 12:57:02 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Wed, 10 Nov 2010 18:45:48 -0800 |
huffman |
section headings
|
changeset |
files
|
| Wed, 10 Nov 2010 18:37:11 -0800 |
huffman |
reorder chapters for generated document
|
changeset |
files
|
| Wed, 10 Nov 2010 18:30:17 -0800 |
huffman |
merge Representable.thy into Domain.thy
|
changeset |
files
|
| Wed, 10 Nov 2010 18:15:21 -0800 |
huffman |
move stuff from Domain.thy to Domain_Aux.thy
|
changeset |
files
|
| Wed, 10 Nov 2010 17:56:08 -0800 |
huffman |
move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
|
changeset |
files
|
| Wed, 10 Nov 2010 14:59:52 -0800 |
huffman |
allow unpointed lazy arguments for definitional domain package
|
changeset |
files
|
| Wed, 10 Nov 2010 14:20:47 -0800 |
huffman |
add lemmas lub_below, below_lub; simplify some proofs; remove some unused lemmas
|
changeset |
files
|
| Wed, 10 Nov 2010 13:22:39 -0800 |
huffman |
merged
|
changeset |
files
|
| Wed, 10 Nov 2010 13:08:42 -0800 |
huffman |
removed unused lemma chain_mono2
|
changeset |
files
|
| Wed, 10 Nov 2010 11:42:35 -0800 |
huffman |
rename class 'bifinite' to 'domain'
|
changeset |
files
|
| Wed, 10 Nov 2010 09:59:08 -0800 |
huffman |
instance sum :: (predomain, predomain) predomain
|
changeset |
files
|
| Wed, 10 Nov 2010 09:52:50 -0800 |
huffman |
configure sum type for fixrec
|
changeset |
files
|
| Wed, 10 Nov 2010 08:18:32 -0800 |
huffman |
add class liftdomain, for bifinite domains where DEFL('a u) = u_defl('a)
|
changeset |
files
|
| Wed, 10 Nov 2010 06:02:37 -0800 |
huffman |
instance prod :: (predomain, predomain) predomain
|
changeset |
files
|
| Tue, 09 Nov 2010 19:37:11 -0800 |
huffman |
adapt isodefl proof script to unpointed types
|
changeset |
files
|
| Tue, 09 Nov 2010 16:37:13 -0800 |
huffman |
add 'predomain' class: unpointed version of bifinite
|
changeset |
files
|
| Tue, 09 Nov 2010 08:41:36 -0800 |
huffman |
add bifiniteness check for domain_isomorphism command
|
changeset |
files
|
| Tue, 09 Nov 2010 05:23:34 -0800 |
huffman |
implement map_of_typ using Pattern.rewrite_term
|
changeset |
files
|
| Tue, 09 Nov 2010 04:47:46 -0800 |
huffman |
avoid using stale theory
|
changeset |
files
|
| Mon, 08 Nov 2010 15:13:45 -0800 |
huffman |
implement defl_of_typ using Pattern.rewrite_term instead of DeflData theory data
|
changeset |
files
|
| Mon, 08 Nov 2010 14:36:17 -0800 |
huffman |
add function the_sort
|
changeset |
files
|
| Mon, 08 Nov 2010 14:09:07 -0800 |
huffman |
refactor tmp_thy code
|
changeset |
files
|
| Mon, 08 Nov 2010 06:58:09 -0800 |
huffman |
reorganize Bifinite.thy; simplify some proofs related to bifinite class instances
|
changeset |
files
|
| Fri, 12 Nov 2010 11:36:01 +0100 |
wenzelm |
treat pervasive "Interrupt" constructor as illegal -- superseded by Exn.Interrupt for internal use and Exn.is_interrupt/Exn.interrupt in user-space;
|
changeset |
files
|