| Sun, 06 Jan 2019 15:04:34 +0100 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Tue, 28 Aug 2018 10:58:43 +0200 |
wenzelm |
clarified signature: do not expose internal operation;
|
file |
diff |
annotate
|
| Thu, 15 Feb 2018 12:11:00 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Thu, 11 Jan 2018 13:48:17 +0100 |
wenzelm |
uniform use of Standard ML op-infix -- eliminated warnings;
|
file |
diff |
annotate
|
| Thu, 11 Jan 2018 12:32:07 +0100 |
wenzelm |
proper infix;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Thu, 26 May 2016 17:51:22 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Sun, 24 Jan 2016 15:30:32 +0100 |
wenzelm |
clarified exception handling;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:54:56 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Sun, 05 Jul 2015 15:02:30 +0200 |
wenzelm |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
file |
diff |
annotate
|
| Sat, 30 May 2015 23:58:06 +0200 |
wenzelm |
standardize towards Thm.eta_long_conversion, which just does eta_long conversion;
|
file |
diff |
annotate
|
| Sat, 30 May 2015 23:30:54 +0200 |
wenzelm |
tuned spelling;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 19:39:05 +0200 |
wenzelm |
tuned -- avoid exotic Name_Space.defined_entry;
|
file |
diff |
annotate
|
| Mon, 30 Mar 2015 22:34:59 +0200 |
wenzelm |
support for strictly private name space entries;
|
file |
diff |
annotate
|
| Mon, 23 Mar 2015 13:30:59 +0100 |
wenzelm |
support 'for' fixes in rule_tac etc.;
|
file |
diff |
annotate
|
| Fri, 20 Mar 2015 14:48:04 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 20 Mar 2015 11:23:32 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 19 Mar 2015 22:30:57 +0100 |
wenzelm |
more position information;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:54:36 +0100 |
wenzelm |
clarified context;
|
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
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Wed, 11 Feb 2015 18:16:33 +0100 |
wenzelm |
proper context;
|
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
|
| Sat, 08 Nov 2014 12:15:40 +0100 |
wenzelm |
more direct type equality;
|
file |
diff |
annotate
|
| Sun, 21 Sep 2014 20:14:04 +0200 |
wenzelm |
more standard Isabelle/ML operations;
|
file |
diff |
annotate
|
| Sun, 21 Sep 2014 19:53:50 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 22 Jun 2014 06:16:57 +0100 |
sultana |
Metis is being used to emulate E steps;
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 18:15:09 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Wed, 19 Mar 2014 22:10:33 +0100 |
wenzelm |
more explicit Long_Name operations (NB: analyzing qualifiers is inherently fragile);
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 15:57:02 +0000 |
sultana |
added a function that carries out all the reconstruction steps, for improved usability;
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 15:57:02 +0000 |
sultana |
reconstruction framework for LEO-II's TPTP proofs;
|
file |
diff |
annotate
|