| Fri, 29 Nov 2024 17:40:15 +0100 |
wenzelm |
clarified signature: shorten common cases;
|
file |
diff |
annotate
|
| Tue, 18 Apr 2023 22:24:48 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 28 Sep 2021 22:14:44 +0200 |
wenzelm |
clarified antiquotations;
|
file |
diff |
annotate
|
| Fri, 10 Sep 2021 14:59:19 +0200 |
wenzelm |
clarified signature: more scalable operations;
|
file |
diff |
annotate
|
| Sat, 13 Apr 2019 22:06:40 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 13 Apr 2019 16:26:19 +0200 |
wenzelm |
tuned signature -- more ctyp operations;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 20:43:09 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Sun, 02 Jul 2017 20:13:38 +0200 |
haftmann |
proper concept of code declaration wrt. atomicity and Isar declarations
|
file |
diff |
annotate
|
| Thu, 23 Jun 2016 11:01:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 21:28:46 +0200 |
haftmann |
explicit tagging of code equations de-baroquifies interface
|
file |
diff |
annotate
|
| Sun, 29 May 2016 15:40:25 +0200 |
wenzelm |
clarified check_open_spec / read_open_spec;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2016 09:43:11 +0200 |
wenzelm |
support 'assumes' in specifications, e.g. 'definition', 'inductive';
|
file |
diff |
annotate
|
| Thu, 14 Apr 2016 15:33:51 +0200 |
wenzelm |
misc tuning and standardization;
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Sun, 06 Sep 2015 22:14:51 +0200 |
haftmann |
prefer "uncurry" as canonical name for case distinction on products in combinatorial view
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:47:08 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Sun, 05 Jul 2015 15:02:30 +0200 |
wenzelm |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
file |
diff |
annotate
|
| Fri, 10 Apr 2015 18:23:01 +0200 |
blanchet |
renamed ML funs
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:53:52 +0100 |
wenzelm |
clarified context;
|
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
|
| Fri, 06 Mar 2015 00:00:57 +0100 |
wenzelm |
tuned -- more explicit use of context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 22:05:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 20:10:59 +0100 |
wenzelm |
just one data slot per program unit;
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 12:56:06 +0100 |
wenzelm |
proper exception for internal program failure, not user-error;
|
file |
diff |
annotate
|
| Wed, 29 Oct 2014 19:01:49 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 18:45:48 +0200 |
wenzelm |
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 15:54:33 +0200 |
blanchet |
export right sorts
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:57 +0200 |
blanchet |
use compatibility layer
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
pretend code generation is a ctr_sugar plugin
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
named interpretations
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 11:57:52 +0100 |
haftmann |
prefer proof context over background theory
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 14:19:18 +0100 |
wenzelm |
tuned signature and module arrangement;
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 08:31:31 +0100 |
haftmann |
two target language numeral types: integer and natural, as replacement for code_numeral;
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 15:27:10 +0100 |
haftmann |
reform of predicate compiler / quickcheck theories:
|
file |
diff |
annotate
|
| Fri, 11 Jan 2013 08:17:47 +0100 |
haftmann |
explicit references avoid dynamic lookup
|
file |
diff |
annotate
|
| Fri, 04 Jan 2013 20:04:59 +0100 |
haftmann |
note to eliminate dynamic name reference
|
file |
diff |
annotate
|
| Sun, 11 Nov 2012 19:56:02 +0100 |
haftmann |
dropped dead code;
|
file |
diff |
annotate
|
| Mon, 20 Feb 2012 12:37:17 +0100 |
huffman |
use qualified constant names instead of suffixes (from Florian Haftmann)
|
file |
diff |
annotate
|
| Wed, 25 Jan 2012 15:19:04 +0100 |
bulwahn |
generalizing check if size matters because it is different for random and exhaustive testing
|
file |
diff |
annotate
|
| Wed, 21 Dec 2011 09:21:35 +0100 |
bulwahn |
quickcheck_generator command also creates random generators
|
file |
diff |
annotate
|
| Tue, 20 Dec 2011 17:22:31 +0100 |
bulwahn |
generalize ensure_sort_datatype to ensure_sort in quickcheck_common to allow generators for abstract types;
|
file |
diff |
annotate
|
| Mon, 05 Dec 2011 12:36:20 +0100 |
bulwahn |
random reporting compilation returns if counterexample is genuine or potentially spurious, and takes genuine_only option as argument
|
file |
diff |
annotate
|
| Mon, 05 Dec 2011 12:36:19 +0100 |
bulwahn |
the reporting random testing also returns if the counterexample is genuine or potentially spurious
|
file |
diff |
annotate
|
| Mon, 05 Dec 2011 12:36:06 +0100 |
bulwahn |
exhaustive returns if a counterexample is genuine or potentially spurious in the presence of assumptions more correctly
|
file |
diff |
annotate
|
| Mon, 05 Dec 2011 12:36:03 +0100 |
bulwahn |
NEWS
|
file |
diff |
annotate
|
| Mon, 05 Dec 2011 12:36:00 +0100 |
bulwahn |
renaming potential flag to genuine_only flag with an inverse semantics
|
file |
diff |
annotate
|
| Mon, 05 Dec 2011 12:35:05 +0100 |
bulwahn |
dynamic genuine_flag in compilation of random and exhaustive
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 22:14:35 +0100 |
bulwahn |
compilations return genuine flag to quickcheck framework
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 22:14:35 +0100 |
bulwahn |
reporting random compilation also catches match exceptions internally
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 22:14:35 +0100 |
bulwahn |
quickcheck-random compilation also indicates if the counterexample is potentially spurious or not
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 22:14:35 +0100 |
bulwahn |
quickcheck's compilation returns if it is genuine counterexample or a counterexample due to a match exception
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 22:14:35 +0100 |
bulwahn |
removing exception handling now that is caught at some other point;
|
file |
diff |
annotate
|
| Thu, 01 Dec 2011 22:14:35 +0100 |
bulwahn |
quickcheck random can also find potential counterexamples;
|
file |
diff |
annotate
|