| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
changed proof method to handle widen predicate in JinjaThreads
|
changeset |
files
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
added further examples; added mode to code_pred command; tuned; some temporary things in Predicate_Compile_ex
|
changeset |
files
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
processing of tuples in introduction rules
|
changeset |
files
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
added a few tricky examples with tuples; added alternative introduction rules for some constants; corrected mode analysis with negation; improved fetching of definitions
|
changeset |
files
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
developing an executable the operator
|
changeset |
files
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
generalizing singleton with a default value
|
changeset |
files
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
changed elimination preprocessing due to an error with a JinjaThread predicate
|
changeset |
files
|
| Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
added test for higher-order function inductification; added debug messages
|
changeset |
files
|
| Sat, 24 Oct 2009 16:55:40 +0200 |
bulwahn |
added filtering of case constants in the definition retrieval of the predicate compiler
|
changeset |
files
|
| Sat, 24 Oct 2009 16:55:37 +0200 |
bulwahn |
extended core of predicate compiler to expand tuples in introduction rules
|
changeset |
files
|
| Sat, 24 Oct 2009 16:55:35 +0200 |
bulwahn |
added tupled versions of examples for the predicate compiler
|
changeset |
files
|
| Sat, 24 Oct 2009 16:54:32 +0200 |
bulwahn |
moved meta_fun_cong lemma into ML-file; tuned
|
changeset |
files
|