| Fri, 11 Mar 2022 11:19:38 +0100 |
desharna |
generated lemma map_ident_strong for BNFs
|
file |
diff |
annotate
|
| Tue, 19 Oct 2021 14:58:22 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Mon, 18 Dec 2017 11:56:12 +0100 |
traytel |
removed debug output
|
file |
diff |
annotate
|
| Sun, 17 Dec 2017 08:42:59 +0100 |
traytel |
made tactics more robust
|
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
|
| Mon, 14 Mar 2016 12:31:05 +0100 |
blanchet |
strengthened tactics
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 15:18:06 +0100 |
traytel |
derive transfer rule for predicator
|
file |
diff |
annotate
|
| Tue, 16 Feb 2016 22:28:19 +0100 |
traytel |
make predicator a first-class bnf citizen
|
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
|
| Thu, 24 Sep 2015 12:28:15 +0200 |
traytel |
congruence rules for the relator
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 21:44:18 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:47:08 +0200 |
wenzelm |
prefer tactics with explicit context;
|
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, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Thu, 25 Sep 2014 16:35:53 +0200 |
desharna |
generate 'rec_transfer' for datatypes
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 13:53:34 +0200 |
desharna |
generate 'set_transfer' for BNFs
|
file |
diff |
annotate
|
| Mon, 01 Sep 2014 13:23:39 +0200 |
desharna |
generate 'rel_transfer' for BNFs
|
file |
diff |
annotate
|
| Mon, 18 Aug 2014 14:09:09 +0200 |
desharna |
generate 'inj_map_strong' for BNFs
|
file |
diff |
annotate
|
| Mon, 18 Aug 2014 13:46:22 +0200 |
desharna |
renamed 'rel_mono_strong' to 'rel_mono_strong0'
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 13:20:54 +0200 |
desharna |
generate 'rel_map' theorem for BNFs
|
file |
diff |
annotate
|
| Fri, 25 Jul 2014 11:26:10 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 08 May 2014 11:52:44 +0200 |
desharna |
generate 'map_ident' theorem for BNFs
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:26 +0200 |
blanchet |
added 'inj_map' as auxiliary BNF theorem
|
file |
diff |
annotate
|
| Fri, 07 Mar 2014 22:30:58 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Thu, 06 Mar 2014 15:40:33 +0100 |
blanchet |
renamed 'fun_rel' to 'rel_fun'
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 00:09:56 +0100 |
blanchet |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file |
diff |
annotate
|
| Fri, 31 Jan 2014 10:02:36 +0100 |
traytel |
less hermetic tactics
|
file |
diff |
annotate
|
| Wed, 29 Jan 2014 16:35:05 +0100 |
traytel |
made tactic more robust
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
tuned names
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
adjusted comments
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
avoid nested 'Tools' directories
|
file |
diff |
annotate
| base
|