| Thu, 13 May 2010 15:09:42 +0200 |
ballarin |
Fix syntax; apparently constant apply was introduced in an earlier changeset.
|
changeset |
files
|
| Thu, 13 May 2010 14:47:15 +0200 |
ballarin |
Merged.
|
changeset |
files
|
| Thu, 13 May 2010 13:30:16 +0200 |
ballarin |
Add mixin to base morphism, required by class package; cf ab324ffd6f3d.
|
changeset |
files
|
| Thu, 13 May 2010 13:29:43 +0200 |
ballarin |
Remove improper use of mixin in class package.
|
changeset |
files
|
| Thu, 13 May 2010 14:34:05 +0200 |
nipkow |
Multiset: renamed, added and tuned lemmas;
|
changeset |
files
|
| Wed, 12 May 2010 22:33:10 -0700 |
huffman |
use 'subsection' instead of 'section', to maintain 1 chapter per file in generated document
|
changeset |
files
|
| Thu, 13 May 2010 00:44:48 +0200 |
boehmes |
more precise dependencies
|
changeset |
files
|
| Wed, 12 May 2010 23:54:06 +0200 |
boehmes |
updated SMT certificates
|
changeset |
files
|
| Wed, 12 May 2010 23:54:04 +0200 |
boehmes |
layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable
|
changeset |
files
|
| Wed, 12 May 2010 23:54:02 +0200 |
boehmes |
integrated SMT into the HOL image
|
changeset |
files
|
| Wed, 12 May 2010 23:54:01 +0200 |
boehmes |
replaced More_conv.top_conv (which does not re-apply the given conversion to its results, only to the result's subterms) by Simplifier.full_rewrite
|
changeset |
files
|
| Wed, 12 May 2010 23:54:00 +0200 |
boehmes |
use proper context operations (for fresh names of type and term variables, and for hypothetical definitions), monomorphize theorems (instead of terms, necessary for hypothetical definitions made during lambda lifting)
|
changeset |
files
|