| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
changed resolving depending predicates and fetching in the predicate compiler
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
extended mode inference by adding generators; adopted compilation; added some functions for constructing term closures
|
file |
diff |
annotate
|
| Tue, 30 Jun 2009 15:58:12 +0200 |
bulwahn |
commented trancl example; added debug message
|
file |
diff |
annotate
|
| Mon, 29 Jun 2009 12:33:58 +0200 |
bulwahn |
added diagnostic printing; changed proof for parameters; moved code
|
file |
diff |
annotate
|
| Fri, 12 Jun 2009 18:33:58 +0200 |
bulwahn |
added cases to code_pred command
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 22:04:23 +0200 |
bulwahn |
masking proof with a quick-and-dirty step
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 21:37:26 +0200 |
bulwahn |
improved infrastructure of predicate compiler for adding manual introduction rules
|
file |
diff |
annotate
|
| Thu, 11 Jun 2009 12:06:13 +0200 |
bulwahn |
making isatest happy; but misunderstanding remains
|
file |
diff |
annotate
|
| Wed, 10 Jun 2009 21:04:36 +0200 |
bulwahn |
code_pred command now also requires proofs for dependent predicates; changed handling of parameters in introrules of executable function
|
file |
diff |
annotate
|
| Tue, 09 Jun 2009 12:05:22 +0200 |
bulwahn |
refactoring the predicate compiler
|
file |
diff |
annotate
|
| Wed, 20 May 2009 22:24:07 +0200 |
haftmann |
experimental values command
|
file |
diff |
annotate
|
| Mon, 18 May 2009 15:45:42 +0200 |
haftmann |
added example on ML level
|
file |
diff |
annotate
|
| Tue, 12 May 2009 21:17:47 +0200 |
haftmann |
split Predicate_Compile examples into separate theory
|
file |
diff |
annotate
| base
|