| Tue, 22 Oct 2024 17:31:54 +0200 |
Fabian Huch |
clarified: proper return type;
|
file |
diff |
annotate
|
| Thu, 12 Sep 2024 19:46:08 +0200 |
wenzelm |
prefer Pretty.pure_string_of to produce output without markup, instead of cleaning output afterwards;
|
file |
diff |
annotate
|
| Fri, 06 Sep 2024 20:31:20 +0200 |
wenzelm |
more thorough Protocol_Message.clean_output, following Isabelle/Scala;
|
file |
diff |
annotate
|
| Sun, 09 Jun 2024 15:31:33 +0200 |
wenzelm |
more accurate thm "name_hint", using Thm_Name.T;
|
file |
diff |
annotate
|
| Thu, 20 Apr 2023 15:24:31 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 20 Apr 2023 12:50:35 +0200 |
wenzelm |
proper theory_long_name;
|
file |
diff |
annotate
|
| Thu, 20 Apr 2023 11:57:34 +0200 |
wenzelm |
clarified signature: explicitly distinguish theory_base_name vs. theory_long_name;
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Tue, 31 Oct 2017 07:11:03 +0000 |
haftmann |
removed ancient nat-int transfer
|
file |
diff |
annotate
|
| Mon, 10 Apr 2017 21:05:31 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 26 Sep 2016 07:56:54 +0200 |
haftmann |
syntactic type class for operation mod named after mod;
|
file |
diff |
annotate
|
| Sat, 05 Mar 2016 17:01:45 +0100 |
wenzelm |
tuned signature -- clarified modules;
|
file |
diff |
annotate
|
| Fri, 03 Jul 2015 14:32:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 01 Jun 2015 18:59:21 +0200 |
haftmann |
separate class for division operator, with particular syntax added in more specific classes
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:39:08 +0200 |
wenzelm |
proper context for Object_Logic operations;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 23:14:05 +0200 |
wenzelm |
local setup of induction tools, with restricted access to auxiliary consts;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Sat, 24 Jan 2015 22:00:24 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 11:36:41 +0100 |
wenzelm |
discontinued obsolete Output.urgent_message;
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
tuned structure inclusion
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 14:59:36 +0200 |
wenzelm |
more uniform ML/document antiquotations;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 12:34:50 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 11:42:32 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Sat, 15 Mar 2014 11:59:18 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 16:54:01 +0100 |
wenzelm |
prefer more robust Synchronized.var;
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 10:23:32 +0100 |
blanchet |
tuned ML file name
|
file |
diff |
annotate
|
| Sat, 13 Jul 2013 00:24:05 +0200 |
wenzelm |
compile
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 23:45:05 +0200 |
wenzelm |
system options for Isabelle/HOL proof tools;
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 11:47:33 +0100 |
haftmann |
systematic conversions between nat and nibble/char;
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 15:27:10 +0100 |
haftmann |
reform of predicate compiler / quickcheck theories:
|
file |
diff |
annotate
|
| Wed, 13 Feb 2013 13:38:52 +0100 |
haftmann |
formal cleanup of sources
|
file |
diff |
annotate
|
| Wed, 19 Sep 2012 10:57:44 +0200 |
bulwahn |
recording elapsed time in mutabelle for more detailed evaluation
|
file |
diff |
annotate
|
| Tue, 24 Apr 2012 09:47:40 +0200 |
blanchet |
handle TPTP definitions as definitions in Nitpick rather than as axioms
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Mon, 27 Feb 2012 16:56:25 +0100 |
wenzelm |
more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 11:23:34 +0100 |
blanchet |
renamed 'try_methods' to 'try0'
|
file |
diff |
annotate
|
| Sat, 11 Feb 2012 12:13:08 +0100 |
bulwahn |
making num_mutations a configuration that can be changed with the mutabelle bash command
|
file |
diff |
annotate
|
| 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
|