| Fri, 20 Apr 2012 20:29:44 +0200 |
wenzelm |
simplified internal actor protocol;
|
changeset |
files
|
| Fri, 20 Apr 2012 20:21:22 +0200 |
wenzelm |
builtin timing for main operations;
|
changeset |
files
|
| Fri, 20 Apr 2012 15:49:45 +0200 |
huffman |
add secondary transfer rule for universal quantifiers on non-bi-total relations
|
changeset |
files
|
| Fri, 20 Apr 2012 15:34:33 +0200 |
huffman |
move definition of set_rel into Library/Quotient_Set.thy
|
changeset |
files
|
| Fri, 20 Apr 2012 15:30:13 +0200 |
huffman |
add transfer rule for 'id'
|
changeset |
files
|
| Fri, 20 Apr 2012 14:57:19 +0200 |
huffman |
add new transfer rules and setup for lifting package
|
changeset |
files
|
| Fri, 20 Apr 2012 10:37:00 +0200 |
huffman |
setup_lifting preprocesses forall_transfer rule by unfolding mem_Collect_eq
|
changeset |
files
|
| Fri, 20 Apr 2012 11:17:01 +0200 |
hoelzl |
NEWS
|
changeset |
files
|
| Fri, 20 Apr 2012 11:14:39 +0200 |
hoelzl |
hide code generation facts in the Float theory, they are only exported for Approximation
|
changeset |
files
|
| Fri, 20 Apr 2012 10:47:04 +0200 |
nipkow |
merged
|
changeset |
files
|
| Fri, 20 Apr 2012 10:46:55 +0200 |
nipkow |
forgot to add file
|
changeset |
files
|
| Fri, 20 Apr 2012 10:18:08 +0200 |
huffman |
make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
|
changeset |
files
|
| Thu, 19 Apr 2012 23:18:47 +0200 |
wenzelm |
merged
|
changeset |
files
|
| Thu, 19 Apr 2012 22:21:15 +0200 |
hoelzl |
NEWS
|
changeset |
files
|
| Thu, 19 Apr 2012 22:13:46 +0200 |
hoelzl |
transfer now handles Let
|
changeset |
files
|
| Thu, 19 Apr 2012 20:19:24 +0200 |
nipkow |
merged
|
changeset |
files
|
| Thu, 19 Apr 2012 20:19:13 +0200 |
nipkow |
added revised version of Abs_Int
|
changeset |
files
|
| Thu, 19 Apr 2012 19:36:09 +0200 |
huffman |
add transfer rule for Let
|
changeset |
files
|
| Thu, 19 Apr 2012 19:32:30 +0200 |
huffman |
add code lemmas for word operations
|
changeset |
files
|
| Thu, 19 Apr 2012 19:18:47 +0200 |
haftmann |
tuned whitespace
|
changeset |
files
|
| Thu, 19 Apr 2012 19:18:11 +0200 |
haftmann |
dropped dead code
|
changeset |
files
|
| Thu, 19 Apr 2012 18:24:40 +0200 |
kuncar |
rename no_code to no_abs_code - more appropriate name
|
changeset |
files
|
| Thu, 19 Apr 2012 17:31:34 +0200 |
kuncar |
use tnames for bound variables in rsp thms
|
changeset |
files
|
| Thu, 19 Apr 2012 17:49:08 +0200 |
blanchet |
true delayed evaluation of "SPASS_VERSION" environment variable
|
changeset |
files
|
| Thu, 19 Apr 2012 17:49:02 +0200 |
blanchet |
merged
|
changeset |
files
|
| Thu, 19 Apr 2012 11:14:57 +0200 |
blanchet |
use latest Z3
|
changeset |
files
|
| Thu, 19 Apr 2012 17:32:35 +0200 |
nipkow |
merged
|
changeset |
files
|
| Thu, 19 Apr 2012 17:32:30 +0200 |
nipkow |
reorganised IMP
|
changeset |
files
|
| Thu, 19 Apr 2012 11:55:30 +0200 |
hoelzl |
use real :: float => real as lifting-morphism so we can directlry use the rep_eq theorems
|
changeset |
files
|
| Wed, 18 Apr 2012 14:29:22 +0200 |
hoelzl |
use lifting to introduce floating point numbers
|
changeset |
files
|