| Sat, 11 Feb 2012 11:36:23 +0100 |
bulwahn |
making max_mutants an option that can be changed in the Mutabelle-script
|
file |
diff |
annotate
|
| Sat, 11 Feb 2012 11:36:21 +0100 |
bulwahn |
increase timeout to 30 seconds; changing mutabelle script
|
file |
diff |
annotate
|
| Sun, 05 Feb 2012 17:43:15 +0100 |
bulwahn |
adding some forbidden constant names for mutabelle
|
file |
diff |
annotate
|
| Sun, 05 Feb 2012 17:43:14 +0100 |
bulwahn |
mutabelle ignores theorems with internal constants
|
file |
diff |
annotate
|
| Tue, 31 Jan 2012 09:06:27 +0100 |
bulwahn |
mutabelle must handle the case where quickcheck returns multiple results
|
file |
diff |
annotate
|
| Tue, 24 Jan 2012 09:12:29 +0100 |
bulwahn |
some more constants on mutabelle's blacklist
|
file |
diff |
annotate
|
| Mon, 23 Jan 2012 15:22:33 +0100 |
bulwahn |
adding another internal constant to mutabelle's blacklust
|
file |
diff |
annotate
|
| Mon, 23 Jan 2012 14:08:55 +0100 |
bulwahn |
adding some more forbidden constant names for the mutated conjecture generation
|
file |
diff |
annotate
|
| Mon, 23 Jan 2012 11:59:00 +0100 |
bulwahn |
more configurations to mutabelle
|
file |
diff |
annotate
|
| Wed, 09 Nov 2011 19:01:50 +0100 |
bulwahn |
quickcheck invocations in mutabelle must not catch codegenerator errors internally
|
file |
diff |
annotate
|
| Mon, 07 Nov 2011 22:21:57 +0100 |
blanchet |
revived Refute in Mutabelle
|
file |
diff |
annotate
|
| Tue, 18 Oct 2011 15:27:17 +0200 |
bulwahn |
adding testing of quickcheck narrowing with finite types to mutabelle script; modified is_executable in mutabelle_extra
|
file |
diff |
annotate
|
| Mon, 17 Oct 2011 10:19:01 +0200 |
bulwahn |
moving some common functions from quickcheck to the more HOL-specific quickcheck_common; renamed inductive_SML's configurations to more canonical names; adds automatically left and right hand sides of equations as evaluation terms
|
file |
diff |
annotate
|
| Fri, 09 Sep 2011 00:22:18 +0200 |
krauss |
added syntactic classes for "inf" and "sup"
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 09:52:09 -0700 |
huffman |
moved division ring stuff from Rings.thy to Fields.thy
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 10:34:21 +0200 |
bulwahn |
adapting mutabelle to latest changes in quickcheck; removing unused code in mutabelle
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 15:39:55 +0200 |
wenzelm |
pervasive Output operations;
|
file |
diff |
annotate
|
| Tue, 07 Jun 2011 14:06:12 +0200 |
bulwahn |
printing environment in mutabelle's log
|
file |
diff |
annotate
|
| Tue, 31 May 2011 17:15:14 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
renamed "Auto_Tools" "Try"
|
file |
diff |
annotate
|
| Wed, 20 Apr 2011 17:17:01 +0200 |
wenzelm |
merged;
|
file |
diff |
annotate
|
| Wed, 20 Apr 2011 16:00:46 +0200 |
bulwahn |
adding two further code-generator internal constants to the blacklist of Mutabelle
|
file |
diff |
annotate
|
| Wed, 20 Apr 2011 16:49:52 +0200 |
wenzelm |
standardized some ML aliases;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Thu, 31 Mar 2011 11:16:51 +0200 |
blanchet |
added support for "dest:" to "try"
|
file |
diff |
annotate
|
| Wed, 23 Mar 2011 08:50:32 +0100 |
bulwahn |
adapting mutabelle; exporting more Quickcheck functions
|
file |
diff |
annotate
|
| Mon, 21 Mar 2011 08:29:16 +0100 |
bulwahn |
merged
|
file |
diff |
annotate
|
| Fri, 18 Mar 2011 18:19:42 +0100 |
bulwahn |
adapting mutabelle
|
file |
diff |
annotate
|
| Sun, 20 Mar 2011 22:08:12 +0100 |
wenzelm |
simplified various cpu_time clones (!): eliminated odd Exn.capture/Exn.release (no need to "stop" timing);
|
file |
diff |
annotate
|
| Sun, 20 Mar 2011 21:28:11 +0100 |
wenzelm |
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
|
file |
diff |
annotate
|
| Fri, 18 Mar 2011 22:55:28 +0100 |
blanchet |
added "simp:", "intro:", and "elim:" to "try" command
|
file |
diff |
annotate
|
| Fri, 11 Feb 2011 11:47:44 +0100 |
bulwahn |
adjusting HOL-Mutabelle to changes in quickcheck
|
file |
diff |
annotate
|
| Mon, 10 Jan 2011 15:45:46 +0100 |
wenzelm |
eliminated Int.toString;
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 12:25:22 +0100 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 12:22:38 +0100 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 11:31:06 +0100 |
bulwahn |
reactivating nitpick in Mutabelle
|
file |
diff |
annotate
|
| Fri, 10 Dec 2010 14:10:35 +0100 |
bulwahn |
setting finite_type_size to 1 in mutabelle_extra
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 10:52:45 +0100 |
bulwahn |
commenting out sledgehammer_mtd in Mutabelle
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 10:52:44 +0100 |
bulwahn |
adding timeout to try invocation in mutabelle
|
file |
diff |
annotate
|
| Mon, 06 Dec 2010 10:52:43 +0100 |
bulwahn |
adding filtering, sytactic welltyping, and sledgehammer method in mutabelle
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 10:28:39 +0100 |
blanchet |
compile
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 09:55:45 +0100 |
blanchet |
run synchronous Auto Tools in parallel
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
adapting mutabelle
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
adapting mutabelle
|
file |
diff |
annotate
|
| Mon, 22 Nov 2010 11:34:59 +0100 |
bulwahn |
adding AFP tests to Mutabelle_Extra; adopting mutabelle to recent quickcheck changes; filtering strange mutants; adding solvers to mutabelle; restructuring mutabelle
|
file |
diff |
annotate
|
| Fri, 05 Nov 2010 19:47:20 +0100 |
wenzelm |
explicit indication of some remaining violations of the Isabelle/ML interrupt model;
|
file |
diff |
annotate
|
| Tue, 02 Nov 2010 20:55:12 +0100 |
wenzelm |
simplified some time constants;
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 08:44:49 +0200 |
bulwahn |
adapting HOL-Mutabelle to changes in quickcheck
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 21:06:56 +0200 |
wenzelm |
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 15:08:51 +0200 |
wenzelm |
added XML.content_of convenience -- cover XML.body, which is the general situation;
|
file |
diff |
annotate
|
| Sat, 11 Sep 2010 10:35:00 +0200 |
blanchet |
finished renaming "Auto_Counterexample" to "Auto_Tools"
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 17:23:03 +0200 |
bulwahn |
removing report from the arguments of the quickcheck functions and refering to it by picking it from the context
|
file |
diff |
annotate
|
| Sun, 05 Sep 2010 19:47:40 +0200 |
wenzelm |
pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 19:34:23 +0200 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
| Sat, 08 May 2010 17:10:27 +0200 |
wenzelm |
prefer Thm.get_name_hint, which is closer to a user-space idea of "theorem name";
|
file |
diff |
annotate
|
| Wed, 05 May 2010 18:25:34 +0200 |
haftmann |
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
|
file |
diff |
annotate
|