| Thu, 26 Jan 2012 09:52:47 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Wed, 25 Jan 2012 16:07:48 +0100 |
bulwahn |
adding very basic code generation to Wellfounded theory
|
changeset |
files
|
| Wed, 25 Jan 2012 16:07:41 +0100 |
bulwahn |
removing dead code from Mutabelle; tuned
|
changeset |
files
|
| Wed, 25 Jan 2012 15:19:04 +0100 |
bulwahn |
generalizing check if size matters because it is different for random and exhaustive testing
|
changeset |
files
|
| Wed, 25 Jan 2012 09:50:34 +0100 |
bulwahn |
merged
|
changeset |
files
|
| Wed, 25 Jan 2012 09:32:23 +0100 |
bulwahn |
adding code equation for Collect on finite types
|
changeset |
files
|
| Tue, 24 Jan 2012 16:00:51 +0100 |
berghofe |
Use lookup_size rather than Datatype.get_info in is_poly to avoid
|
changeset |
files
|
| Tue, 24 Jan 2012 09:13:24 +0100 |
bulwahn |
adding some rules to quickcheck's preprocessing
|
changeset |
files
|
| Tue, 24 Jan 2012 09:12:29 +0100 |
bulwahn |
some more constants on mutabelle's blacklist
|
changeset |
files
|
| Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
implemented "tptp_refute" tool
|
changeset |
files
|
| Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
added problem importer
|
changeset |
files
|
| Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
imported patch ATP_Problem_Import.thy
|
changeset |
files
|
| Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
imported patch atp_problem_import.ML
|
changeset |
files
|
| Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
renamed theory exporter
|
changeset |
files
|
| Mon, 23 Jan 2012 17:40:32 +0100 |
blanchet |
renamed two files to make room for a new file
|
changeset |
files
|
| Mon, 23 Jan 2012 17:40:31 +0100 |
blanchet |
rebranded Nitrox, for more uniformity
|
changeset |
files
|
| Mon, 23 Jan 2012 17:40:31 +0100 |
blanchet |
moved "nitrox" to TPTP
|
changeset |
files
|
| Mon, 23 Jan 2012 17:29:19 +0100 |
huffman |
generalize type of List.listrel
|
changeset |
files
|
| Mon, 23 Jan 2012 15:23:02 +0100 |
bulwahn |
support for Ex1 in quickcheck-narrowing
|
changeset |
files
|
| Mon, 23 Jan 2012 15:22:33 +0100 |
bulwahn |
adding another internal constant to mutabelle's blacklust
|
changeset |
files
|
| Mon, 23 Jan 2012 14:08:55 +0100 |
bulwahn |
adding some more forbidden constant names for the mutated conjecture generation
|
changeset |
files
|
| Mon, 23 Jan 2012 14:07:36 +0100 |
bulwahn |
adding code generation for some list relations
|
changeset |
files
|
| Mon, 23 Jan 2012 14:06:19 +0100 |
bulwahn |
adding fun_eq_iff to the preprocessing
|
changeset |
files
|
| Mon, 23 Jan 2012 14:00:52 +0100 |
bulwahn |
random instance for sets
|
changeset |
files
|
| Mon, 23 Jan 2012 11:59:00 +0100 |
bulwahn |
more configurations to mutabelle
|
changeset |
files
|
| Fri, 20 Jan 2012 09:28:54 +0100 |
bulwahn |
catching code generation errors in quickcheck-narrowing
|
changeset |
files
|
| Fri, 20 Jan 2012 09:28:53 +0100 |
bulwahn |
adding narrowing instance for sets
|
changeset |
files
|
| Fri, 20 Jan 2012 09:28:52 +0100 |
bulwahn |
shortened definitions by adding some termify constants
|
changeset |
files
|
| Fri, 20 Jan 2012 09:28:51 +0100 |
bulwahn |
tuned
|
changeset |
files
|
| Fri, 20 Jan 2012 09:28:50 +0100 |
bulwahn |
adding check_all instance for sets; tuned
|
changeset |
files
|
| Fri, 20 Jan 2012 08:24:51 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Fri, 20 Jan 2012 07:55:43 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Thu, 19 Jan 2012 21:37:12 +0100 |
blanchet |
minor edits in docs
|
changeset |
files
|
| Thu, 19 Jan 2012 21:37:12 +0100 |
blanchet |
renamed "sound" option to "strict"
|
changeset |
files
|
| Thu, 19 Jan 2012 21:37:12 +0100 |
blanchet |
updated Sledge docs some more
|
changeset |
files
|
| Thu, 19 Jan 2012 21:37:12 +0100 |
blanchet |
more doc updates
|
changeset |
files
|
| Thu, 19 Jan 2012 21:37:12 +0100 |
blanchet |
updated docs
|
changeset |
files
|
| Thu, 19 Jan 2012 21:37:12 +0100 |
blanchet |
lower timeout for preplay, now that we have more preplay methods
|
changeset |
files
|
| Thu, 19 Jan 2012 21:37:12 +0100 |
blanchet |
cleanly separate each Metis encoding
|
changeset |
files
|
| Thu, 09 Feb 2012 19:34:23 +0100 |
wenzelm |
basic setup for equational reasoning;
|
changeset |
files
|
| Tue, 07 Feb 2012 18:56:40 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 07 Feb 2012 18:51:22 +0100 |
wenzelm |
updated examples for syntax translations;
|
changeset |
files
|
| Sun, 05 Feb 2012 21:00:38 +0100 |
wenzelm |
updated section on raw syntax;
|
changeset |
files
|
| Sun, 05 Feb 2012 18:11:19 +0100 |
wenzelm |
updated section about syntax ambiguity;
|
changeset |
files
|
| Sat, 04 Feb 2012 18:33:04 +0100 |
wenzelm |
updated/unified section on mixfix annotations;
|
changeset |
files
|
| Sat, 04 Feb 2012 16:08:19 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sat, 04 Feb 2012 15:56:49 +0100 |
wenzelm |
more on explicit notation;
|
changeset |
files
|
| Sat, 04 Feb 2012 15:44:50 +0100 |
wenzelm |
more accurate Pure grammar;
|
changeset |
files
|
| Sat, 04 Feb 2012 14:25:14 +0100 |
wenzelm |
more refs;
|
changeset |
files
|
| Sat, 04 Feb 2012 14:20:39 +0100 |
wenzelm |
simplified mixfix (NB: infix is no longer required separately);
|
changeset |
files
|
| Thu, 02 Feb 2012 21:21:41 +0100 |
wenzelm |
updated section on print modes;
|
changeset |
files
|
| Thu, 02 Feb 2012 20:26:44 +0100 |
wenzelm |
misc tuning and reformatting;
|
changeset |
files
|
| Thu, 02 Feb 2012 18:11:42 +0100 |
wenzelm |
clarified syntax section structure;
|
changeset |
files
|
| Thu, 02 Feb 2012 17:52:16 +0100 |
wenzelm |
discontinued obscure history commands;
|
changeset |
files
|
| Thu, 02 Feb 2012 16:38:15 +0100 |
wenzelm |
misc tuning and reformatting;
|
changeset |
files
|
| Thu, 02 Feb 2012 16:07:25 +0100 |
wenzelm |
discontinued obscure history commands;
|
changeset |
files
|
| Sun, 29 Jan 2012 22:12:25 +0100 |
wenzelm |
updated hint about asm_rl;
|
changeset |
files
|
| Sun, 29 Jan 2012 22:00:10 +0100 |
wenzelm |
updated thin_tac;
|
changeset |
files
|
| Sun, 29 Jan 2012 21:40:29 +0100 |
wenzelm |
updated distinct_subgoals_tac, flexflex_tac;
|
changeset |
files
|
| Sun, 29 Jan 2012 21:26:09 +0100 |
wenzelm |
removed obscure material;
|
changeset |
files
|