Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
cleaning the signature of the predicate compiler core; renaming signature and structures to uniform long names
|
file |
diff |
annotate
|
Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
added option show_mode_inference; added splitting of conjunctions in expand_tuples
|
file |
diff |
annotate
|
Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
changed import_intros to handle parameters differently; changed handling of higher-order function compilation; reverted MicroJava change; tuned
|
file |
diff |
annotate
|
Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
cleaned up debugging messages; added options to code_pred command
|
file |
diff |
annotate
|
Sat, 24 Oct 2009 16:55:42 +0200 |
bulwahn |
added theory with alternative definitions for the predicate compiler; cleaned up examples
|
file |
diff |
annotate
|
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
|
file |
diff |
annotate
|
Sat, 24 Oct 2009 16:55:40 +0200 |
bulwahn |
added filtering of case constants in the definition retrieval of the predicate compiler
|
file |
diff |
annotate
|
Sat, 24 Oct 2009 16:54:32 +0200 |
bulwahn |
moved meta_fun_cong lemma into ML-file; tuned
|
file |
diff |
annotate
|
Wed, 21 Oct 2009 17:34:35 +0200 |
blanchet |
renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
|
file |
diff |
annotate
|
Sat, 17 Oct 2009 16:58:03 +0200 |
wenzelm |
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
|
file |
diff |
annotate
|
Sat, 17 Oct 2009 15:57:51 +0200 |
wenzelm |
indicate CRITICAL nature of various setmp combinators;
|
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 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
|