| Mon, 30 Jan 2012 13:55:26 +0100 |
bulwahn |
renaming all lemmas with name rel_pow to relpow
|
changeset |
files
|
| Mon, 30 Jan 2012 13:55:24 +0100 |
bulwahn |
adding code equations for max_extp and mlex
|
changeset |
files
|
| Mon, 30 Jan 2012 13:55:23 +0100 |
bulwahn |
adding code generation for relpow by copying the ideas for code generation of funpow
|
changeset |
files
|
| Mon, 30 Jan 2012 13:55:22 +0100 |
bulwahn |
adding code equation for rtranclp in Enum
|
changeset |
files
|
| Mon, 30 Jan 2012 13:55:21 +0100 |
bulwahn |
adding code equation for max_ext
|
changeset |
files
|
| Mon, 30 Jan 2012 13:55:20 +0100 |
bulwahn |
adding code equation for tranclp
|
changeset |
files
|
| Mon, 30 Jan 2012 13:55:19 +0100 |
bulwahn |
adding code_unfold to make measure executable
|
changeset |
files
|
| Sun, 29 Jan 2012 15:16:27 +0100 |
nipkow |
removed accidental dependance of abstract interpreter on gamma
|
changeset |
files
|
| Sun, 29 Jan 2012 10:34:02 +0100 |
nipkow |
merged
|
changeset |
files
|
| Sun, 29 Jan 2012 10:33:54 +0100 |
nipkow |
tuned
|
changeset |
files
|
| Sat, 28 Jan 2012 12:05:26 +0100 |
bulwahn |
an executable version of accessible part (only for finite types yet)
|
changeset |
files
|
| Sat, 28 Jan 2012 10:35:52 +0100 |
bulwahn |
adding yet another induction rule on natural numbers
|
changeset |
files
|
| Sat, 28 Jan 2012 10:22:46 +0100 |
bulwahn |
moving declarations back to the section they seem to belong to (cf. afffe1f72143)
|
changeset |
files
|
| Sat, 28 Jan 2012 06:13:03 +0100 |
bulwahn |
reverting 46c2c96f5d92 as it only provides mostly non-terminating executions for generated code
|
changeset |
files
|
| Fri, 27 Jan 2012 19:08:48 +0100 |
bulwahn |
adding some more examples for quickcheck; replaced FIXME comments
|
changeset |
files
|
| Fri, 27 Jan 2012 17:22:05 +0100 |
bulwahn |
new code equation for ntrancl that allows computation of the transitive closure of sets on infinite types as well
|
changeset |
files
|
| Fri, 27 Jan 2012 17:02:08 +0100 |
nipkow |
removed duplicate definitions that made locale inconsistent
|
changeset |
files
|
| Fri, 27 Jan 2012 14:30:44 +0100 |
nipkow |
added parity analysis
|
changeset |
files
|
| Fri, 27 Jan 2012 10:31:31 +0100 |
bulwahn |
corrected expectation; added an example for quickcheck
|
changeset |
files
|
| Fri, 27 Jan 2012 10:31:30 +0100 |
bulwahn |
adding some basic handling that unfolds a conjecture in a locale before testing it with quickcheck
|
changeset |
files
|
| Fri, 27 Jan 2012 10:19:55 +0100 |
blanchet |
made SML/NJ happy
|
changeset |
files
|
| Thu, 26 Jan 2012 20:49:54 +0100 |
blanchet |
even more lr tags for SPASS -- anything that is considered an "equational rule spec" is relevant
|
changeset |
files
|
| Thu, 26 Jan 2012 20:49:54 +0100 |
blanchet |
separate orthogonal components
|
changeset |
files
|
| Thu, 26 Jan 2012 20:49:54 +0100 |
blanchet |
generate left-to-right rewrite tag for combinator helpers for SPASS 3.8
|
changeset |
files
|
| Thu, 26 Jan 2012 20:49:54 +0100 |
blanchet |
better handling of individual type for DFG format (SPASS)
|
changeset |
files
|
| Thu, 26 Jan 2012 12:04:05 +0100 |
bulwahn |
adding quickcheck example with THE
|
changeset |
files
|
| Thu, 26 Jan 2012 12:03:35 +0100 |
bulwahn |
evaluation of THE with a non-singleton set raises a Match exception during the evaluation to yield a potential counterexample in quickcheck.
|
changeset |
files
|
| Thu, 26 Jan 2012 10:59:47 +0100 |
bulwahn |
using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4
|
changeset |
files
|
| 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
|