| Wed, 28 Aug 2024 22:54:45 +0200 |
wenzelm |
more specific "args" syntax, to support more markup for syntax consts;
|
file |
diff |
annotate
|
| Sun, 15 Jan 2023 18:30:18 +0100 |
wenzelm |
isabelle update -u cite;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2022 20:22:13 +0200 |
wenzelm |
proper umlauts;
|
file |
diff |
annotate
|
| Mon, 27 Jun 2022 17:36:26 +0200 |
traytel |
tuned BNF bounds for function space and bounded sets; NEWS and CONTRIBUTORS
|
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
|
| Wed, 03 Nov 2021 11:02:36 +0100 |
traytel |
add documentation for pred_mono
|
file |
diff |
annotate
|
| Fri, 17 Apr 2020 17:32:11 +0200 |
blanchet |
removed LaTeX package and hack to avoid ALLCAPS headers
|
file |
diff |
annotate
|
| Fri, 28 Feb 2020 21:23:11 +0100 |
traytel |
tuned lift_bnf's user interface for quotients
|
file |
diff |
annotate
|
| Sun, 19 Jan 2020 07:50:35 +0100 |
traytel |
new examples of BNF lifting across quotients using a new theory of confluence,
|
file |
diff |
annotate
|
| Tue, 07 Jan 2020 14:58:01 +0100 |
traytel |
eliminated one redundant proof obligation in lift_bnf for quotients
|
file |
diff |
annotate
|
| Tue, 10 Dec 2019 01:06:39 +0100 |
traytel |
NEWS, CONTRIBUTORS, and documentation
|
file |
diff |
annotate
|
| Fri, 11 Oct 2019 11:08:32 +0200 |
blanchet |
document antiquotations + clarify porting text slightly
|
file |
diff |
annotate
|
| Thu, 10 Oct 2019 16:37:52 +0200 |
blanchet |
added para constrasting 'primrec' and 'fun' -- and removed my middle name
|
file |
diff |
annotate
|
| Sun, 07 Apr 2019 08:26:57 +0200 |
traytel |
bundle for cardinal syntax
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Wed, 26 Dec 2018 16:25:20 +0100 |
wenzelm |
isabelle update_cartouches -t;
|
file |
diff |
annotate
|
| Fri, 22 Jun 2018 20:31:49 +0200 |
wenzelm |
clarified document antiquotation @{theory};
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Tue, 02 Jan 2018 21:32:14 +0100 |
blanchet |
removed para about 'old_datatype' in docs
|
file |
diff |
annotate
|
| Tue, 02 Jan 2018 20:38:41 +0100 |
wenzelm |
old_datatype no longer exists (cf. 706b1cf7b76d);
|
file |
diff |
annotate
|
| Fri, 18 Aug 2017 20:47:47 +0200 |
wenzelm |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
file |
diff |
annotate
|
| Mon, 23 Jan 2017 17:35:37 +0100 |
traytel |
tuned documentation
|
file |
diff |
annotate
|
| Fri, 12 Aug 2016 17:53:55 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Thu, 11 Aug 2016 18:26:44 +0200 |
wenzelm |
clarified antiquotations;
|
file |
diff |
annotate
|
| Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|
| Wed, 30 Mar 2016 15:16:50 +0200 |
blanchet |
more 'corec' docs
|
file |
diff |
annotate
|
| Tue, 29 Mar 2016 21:25:19 +0200 |
blanchet |
more 'corec' docs
|
file |
diff |
annotate
|
| Tue, 29 Mar 2016 09:49:39 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:50:10 +0100 |
blanchet |
updated doc
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 17:21:43 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 16:26:50 +0100 |
traytel |
adjust 112eefe85ff0 to 532ad8de5d61
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 15:18:06 +0100 |
traytel |
correct (apparently untested) e1698a9578ea
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 15:18:06 +0100 |
traytel |
document predicator in datatypes
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 11:39:26 +0100 |
traytel |
call the predicator of list list_all
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 12:07:49 +0100 |
blanchet |
document new 'primrec' feature
|
file |
diff |
annotate
|
| Tue, 16 Feb 2016 22:28:19 +0100 |
traytel |
make predicator a first-class bnf citizen
|
file |
diff |
annotate
|
| Mon, 15 Feb 2016 12:47:16 +0100 |
blanchet |
document a limitation of 'primcorec'
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 15:53:39 +0100 |
wenzelm |
more uniform treatment of package internals;
|
file |
diff |
annotate
|
| Wed, 06 Jan 2016 13:04:31 +0100 |
blanchet |
updated docs
|
file |
diff |
annotate
|
| Fri, 04 Dec 2015 22:19:04 +0100 |
blanchet |
tuned docs
|
file |
diff |
annotate
|
| Fri, 04 Dec 2015 21:39:38 +0100 |
blanchet |
more documentation on 'size' plugin
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Wed, 07 Oct 2015 13:34:42 +0200 |
blanchet |
clarify docs
|
file |
diff |
annotate
|
| Wed, 07 Oct 2015 10:42:13 +0200 |
blanchet |
updated docs
|
file |
diff |
annotate
|
| Wed, 07 Oct 2015 10:02:58 +0200 |
blanchet |
made documentation more accurate
|
file |
diff |
annotate
|
| Thu, 01 Oct 2015 18:59:53 +0200 |
blanchet |
tuned documentation
|
file |
diff |
annotate
|
| Thu, 01 Oct 2015 18:44:48 +0200 |
blanchet |
tuned datatype docs
|
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 |
more useful properties of the relators
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Wed, 12 Aug 2015 20:46:33 +0200 |
traytel |
NEWS, CONTRIBUTORS, documentation for lift_bnf
|
file |
diff |
annotate
|
| Thu, 16 Jul 2015 17:25:44 +0200 |
blanchet |
generalized limitation in documentation
|
file |
diff |
annotate
|
| Mon, 25 May 2015 22:11:43 +0200 |
wenzelm |
merged, resolving conflicts in Admin/isatest/settings/afp-poly and src/HOL/Tools/Nitpick/nitpick_model.ML;
|
file |
diff |
annotate
|
| Wed, 06 May 2015 14:23:22 +0200 |
blanchet |
corrected path in doc
|
file |
diff |
annotate
|
| Wed, 22 Apr 2015 19:52:29 +0200 |
blanchet |
doc
|
file |
diff |
annotate
|
| Wed, 06 May 2015 15:04:38 +0200 |
blanchet |
added acknowledgment
|
file |
diff |
annotate
|
| Tue, 28 Apr 2015 22:56:28 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 22 Apr 2015 20:07:00 +0200 |
blanchet |
improved docs
|
file |
diff |
annotate
|