| 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
|
| Mon, 12 Sep 2016 19:22:37 +0200 |
blanchet |
moved ML function
|
file |
diff |
annotate
|
| Thu, 02 Jun 2016 17:05:40 +0200 |
wenzelm |
clarified aliases (no warning for duplicates);
|
file |
diff |
annotate
|
| Fri, 27 May 2016 20:23:55 +0200 |
wenzelm |
tuned proofs, to allow unfold_abs_def;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2015 20:57:35 +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 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, 31 Mar 2015 15:29:09 +0200 |
wenzelm |
more standard Long_Name operations;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2015 20:34:14 +0100 |
wenzelm |
tuned;
|
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 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2015 19:08:04 +0100 |
traytel |
eliminated some clones of Proof_Context.cterm_of
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 11:18:58 +0100 |
desharna |
generate 'disc_eq_case' for Ctr_Sugars
|
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
|
| 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
|
| Tue, 09 Sep 2014 20:51:36 +0200 |
blanchet |
nicer case names in the N2M case, similar to those generated by the old package (e.g. 'Cons_tree' instead of just 'Cons')
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 19:21:07 +0200 |
blanchet |
honour sorts in N2M
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 15:11:37 +0200 |
blanchet |
use right sort constraints
|
file |
diff |
annotate
|
| Mon, 08 Sep 2014 14:03:08 +0200 |
blanchet |
wildcards in plugins
|
file |
diff |
annotate
|
| Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
added 'plugins' option to control which hooks are enabled
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 10:50:28 +0200 |
desharna |
generate 'set_induct' theorem for codatatypes
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
repaired named derivations
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
use the noted theorem whenever possible, also in 'BNF_Def'
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
use termtab instead of (perhaps overly sensitive) thmtab
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)
|
file |
diff |
annotate
|
| Thu, 17 Jul 2014 10:28:32 +0200 |
desharna |
add mk_Trueprop_mem utility function
|
file |
diff |
annotate
|
| Mon, 07 Jul 2014 16:06:46 +0200 |
desharna |
add helper function map_prod
|
file |
diff |
annotate
|
| Mon, 26 May 2014 16:32:55 +0200 |
blanchet |
got rid of '=:' squiggly
|
file |
diff |
annotate
|
| Mon, 26 May 2014 16:32:51 +0200 |
blanchet |
use '%x. x = C' as default discriminator for nullary constructor C, instead of relying on odd '=:' syntax
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 18:19:57 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 13:31:42 +0100 |
blanchet |
name derivations in 'primrec' for code extraction from proof terms
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 15:03:24 +0100 |
blanchet |
allow different functions to recurse on the same type, like in the old package
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
more precise spec rules for selectors
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:46 +0100 |
blanchet |
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
|
file |
diff |
annotate
|
| Mon, 09 Dec 2013 09:44:57 +0100 |
blanchet |
tuning -- moved ML files to subdirectory
|
file |
diff |
annotate
| base
|