| Mon, 27 Jun 2022 15:54:18 +0200 |
traytel |
strict bounds for BNFs (by Jan van Brügge)
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Sat, 30 Jul 2016 21:10:02 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2016 21:00:32 +0200 |
blanchet |
killed deadcode
|
file |
diff |
annotate
|
| Thu, 07 Apr 2016 17:56:26 +0200 |
traytel |
removed duplicate lemma
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
| Sun, 13 Dec 2015 21:56:15 +0100 |
wenzelm |
more general types Proof.method / context_tactic;
|
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
|
| 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, 24 Jul 2015 22:29:06 +0200 |
wenzelm |
eliminated alias;
|
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 16:46:21 +0100 |
wenzelm |
misc tuning;
|
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
|
| Wed, 08 Oct 2014 17:09:07 +0200 |
wenzelm |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
file |
diff |
annotate
|
| Thu, 25 Sep 2014 16:35:53 +0200 |
desharna |
generate 'rec_transfer' for datatypes
|
file |
diff |
annotate
|
| Thu, 25 Sep 2014 16:35:50 +0200 |
desharna |
generate 'ctor_rec_transfer' for datatypes
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:45:42 +0200 |
blanchet |
tuning terminology
|
file |
diff |
annotate
|
| Mon, 18 Aug 2014 13:46:22 +0200 |
desharna |
renamed 'rel_mono_strong' to 'rel_mono_strong0'
|
file |
diff |
annotate
|
| Thu, 07 Aug 2014 09:35:31 +0200 |
traytel |
tuned
|
file |
diff |
annotate
|
| Thu, 31 Jul 2014 13:19:57 +0200 |
traytel |
simplified tactics slightly
|
file |
diff |
annotate
|
| Mon, 28 Apr 2014 00:54:30 +0200 |
blanchet |
cleaner 'rel_inject' theorems
|
file |
diff |
annotate
|
| Wed, 23 Apr 2014 10:23:26 +0200 |
blanchet |
generate size instances for new-style datatypes
|
file |
diff |
annotate
|
| Mon, 24 Mar 2014 16:33:36 +0100 |
traytel |
made tactic more robust
|
file |
diff |
annotate
|
| Mon, 24 Mar 2014 16:33:36 +0100 |
traytel |
inline helper function
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 08:37:43 +0100 |
haftmann |
generalized and strengthened cong rules on compound operators, similar to 1ed737a98198
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 08:13:23 +0100 |
traytel |
simplified internal datatype construction
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 16:28:25 +0100 |
traytel |
tuned tactics
|
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
|
| Tue, 04 Mar 2014 18:57:17 +0100 |
blanchet |
renamed a pair of low-level theorems to have c/dtor in their names (like the others)
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 10:10:38 +0100 |
traytel |
made tactics more robust
|
file |
diff |
annotate
|
| Tue, 18 Feb 2014 14:51:26 +0100 |
traytel |
syntactic simplifications of internal (co)datatype constructions
|
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
|
| 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
|