| Mon, 11 Mar 2024 08:45:55 +0100 |
traytel |
export BNF properties about the cardinal bound (by Jan van Brügge)
|
file |
diff |
annotate
|
| Tue, 23 May 2023 18:46:15 +0200 |
wenzelm |
tuned signature: more position information;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2022 12:32:59 +0200 |
traytel |
separate out definition of bound to avoid spurious sort hypotheses (by Jan van Brügge)
|
file |
diff |
annotate
|
| Mon, 27 Jun 2022 15:54:18 +0200 |
traytel |
strict bounds for BNFs (by Jan van Brügge)
|
file |
diff |
annotate
|
| Fri, 11 Mar 2022 11:19:38 +0100 |
desharna |
generated lemma map_ident_strong for BNFs
|
file |
diff |
annotate
|
| Tue, 02 Nov 2021 13:51:29 +0100 |
desharna |
added "mono" attribute to BNF generated pred_mono theorems
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Mon, 12 Oct 2020 07:25:38 +0000 |
haftmann |
consolidated names and operations
|
file |
diff |
annotate
|
| Fri, 14 Aug 2020 14:40:24 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 09 Aug 2019 17:14:49 +0200 |
wenzelm |
formal position for PThm nodes;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sun, 17 Dec 2017 08:42:59 +0100 |
traytel |
made tactics more robust
|
file |
diff |
annotate
|
| Tue, 11 Jul 2017 21:36:42 +0200 |
traytel |
store the unfolded definitions of the lifted bnf constants under "_def" name
|
file |
diff |
annotate
|
| Tue, 27 Jun 2017 00:07:34 +0200 |
blanchet |
more error checking
|
file |
diff |
annotate
|
| Wed, 21 Dec 2016 12:49:15 +0100 |
blanchet |
generalized ML function (towards nonuniform datatypes)
|
file |
diff |
annotate
|
| Tue, 01 Nov 2016 16:04:35 +0100 |
traytel |
tuned signature
|
file |
diff |
annotate
|
| Tue, 13 Sep 2016 16:23:12 +0200 |
blanchet |
union associates to the left
|
file |
diff |
annotate
|
| Mon, 12 Sep 2016 13:35:29 +0200 |
blanchet |
prove 'set' property backward
|
file |
diff |
annotate
|
| Thu, 18 Aug 2016 11:10:07 +0200 |
traytel |
derive pred_mono property for BNFs
|
file |
diff |
annotate
|
| Tue, 05 Jul 2016 22:47:48 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Fri, 27 May 2016 20:23:55 +0200 |
wenzelm |
tuned proofs, to allow unfold_abs_def;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2016 14:26:21 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 01 Mar 2016 13:11:56 +0100 |
blanchet |
generalized ML function
|
file |
diff |
annotate
|
| Fri, 26 Feb 2016 15:49:35 +0100 |
blanchet |
generalized ML function
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 15:18:06 +0100 |
traytel |
derive transfer rule for predicator
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 11:54:34 +0100 |
blanchet |
allow predicator instead of map function in 'primrec'
|
file |
diff |
annotate
|
| Tue, 16 Feb 2016 22:28:19 +0100 |
traytel |
make predicator a first-class bnf citizen
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 15:53:39 +0100 |
wenzelm |
more uniform treatment of package internals;
|
file |
diff |
annotate
|
| Sun, 13 Dec 2015 21:56:15 +0100 |
wenzelm |
more general types Proof.method / context_tactic;
|
file |
diff |
annotate
|
| Tue, 01 Dec 2015 13:07:40 +0100 |
blanchet |
tuned whitespace
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Tue, 06 Oct 2015 12:01:07 +0200 |
traytel |
collect the names from goals in favor of fragile exports
|
file |
diff |
annotate
|
| Thu, 01 Oct 2015 17:32:07 +0200 |
blanchet |
export '_cmd' functions
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 23:01:31 +0200 |
traytel |
more canonical context threading
|
file |
diff |
annotate
|
| Thu, 24 Sep 2015 12:28:15 +0200 |
traytel |
congruence rules for the relator
|
file |
diff |
annotate
|
| Thu, 24 Sep 2015 12:21:19 +0200 |
traytel |
conceal only the definitional theorems of map, set, rel (and not the actual constants)
|
file |
diff |
annotate
|
| Thu, 24 Sep 2015 12:21:19 +0200 |
traytel |
more useful properties of the relators
|
file |
diff |
annotate
|
| Fri, 04 Sep 2015 21:40:59 +0200 |
wenzelm |
close derivation *before* splitting conjuncts, like Goal.prove_common (see also 757cad5a3fe9) -- potential improvement of performance;
|
file |
diff |
annotate
|
| Thu, 03 Sep 2015 16:41:43 +0200 |
traytel |
use open/close_target rather than Local_Theory.restore to get polymorphic definitions;
|
file |
diff |
annotate
|
| Sun, 16 Aug 2015 18:19:30 +0200 |
wenzelm |
prefer theory_id operations;
|
file |
diff |
annotate
|
| Thu, 13 Aug 2015 13:55:52 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Thu, 13 Aug 2015 11:05:19 +0200 |
wenzelm |
tuned signature, in accordance to sortBy in Scala;
|
file |
diff |
annotate
|
| Wed, 12 Aug 2015 20:46:33 +0200 |
traytel |
new command for lifting BNF structure over typedefs
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2015 17:24:54 +0200 |
wenzelm |
updated to infer_instantiate;
|
file |
diff |
annotate
|
| Fri, 17 Jul 2015 16:13:03 +0200 |
traytel |
forgotten selector
|
file |
diff |
annotate
|
| Thu, 16 Jul 2015 12:23:22 +0200 |
traytel |
{r,e,d,f}tac with proper context in BNF
|
file |
diff |
annotate
|
| Tue, 28 Apr 2015 22:57:07 +0200 |
blanchet |
allow sorts on dead variables in BNFs
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 30 Mar 2015 22:34:59 +0200 |
wenzelm |
support for strictly private name space entries;
|
file |
diff |
annotate
|
| Fri, 27 Mar 2015 09:56:34 +0100 |
blanchet |
sort BNFs in output
|
file |
diff |
annotate
|
| Mon, 16 Mar 2015 23:05:56 +0100 |
traytel |
BNF relators preserve reflexivity
|
file |
diff |
annotate
|
| Tue, 10 Mar 2015 09:49:17 +0100 |
blanchet |
split into subgoals
|
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
|
| Tue, 03 Mar 2015 19:08:04 +0100 |
traytel |
eliminated some clones of Proof_Context.cterm_of
|
file |
diff |
annotate
|
| Mon, 05 Jan 2015 10:09:42 +0100 |
blanchet |
added plugins syntax to prim(co)rec
|
file |
diff |
annotate
|
| Thu, 11 Dec 2014 14:14:39 +0100 |
traytel |
note more facts (always)
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Mon, 03 Nov 2014 14:50:27 +0100 |
wenzelm |
eliminated unused int_only flag (see also c12484a27367);
|
file |
diff |
annotate
|