| Wed, 23 Sep 2009 16:20:13 +0200 |
bulwahn |
replaced sorry by oops; removed old debug functions in predicate compiler
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:13 +0200 |
bulwahn |
added first version of quickcheck based on the predicate compiler; added a few quickcheck examples
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
added a new example for the predicate compiler
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
added context free grammar example; removed dead code; adapted to work without quick and dirty mode; fixed typo
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
added first prototype of the extended predicate compiler
|
file |
diff |
annotate
|
| Wed, 23 Sep 2009 16:20:12 +0200 |
bulwahn |
extending predicate compiler and proof procedure to support tuples; testing predicate wirh HOL-MicroJava semantics
|
file |
diff |
annotate
|
| Tue, 15 Sep 2009 15:22:15 +0200 |
haftmann |
added singleton example
|
file |
diff |
annotate
|
| Thu, 27 Aug 2009 18:45:39 +0200 |
nipkow |
New example: IMP
|
file |
diff |
annotate
|
| Wed, 26 Aug 2009 16:13:19 +0200 |
nipkow |
new interval lemma
|
file |
diff |
annotate
|
| Mon, 10 Aug 2009 13:34:50 +0200 |
haftmann |
properly merged
|
file |
diff |
annotate
|
| Mon, 10 Aug 2009 10:25:00 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Thu, 30 Jul 2009 13:52:18 +0200 |
haftmann |
cleaned up
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
improved use of context with cases rule in predicate compiler; predicate compiler based on Main for faster debugging
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
commented rpred compilation; tuned
|
file |
diff |
annotate
|
| Tue, 04 Aug 2009 08:34:56 +0200 |
bulwahn |
added generator compilation of higher-order predicates; refined mode analysis for generators; some tuning
|
file |
diff |
annotate
|
| 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
|