Tue, 20 Aug 2019 11:01:05 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Wed, 14 Aug 2019 11:14:27 +0200 |
wenzelm |
treat simproc results as atomic -- more compact proof terms;
|
file |
diff |
annotate
|
Tue, 06 Aug 2019 16:29:28 +0200 |
wenzelm |
more robust and convenient treatment of implicit context;
|
file |
diff |
annotate
|
Thu, 03 Jan 2019 14:12:44 +0100 |
wenzelm |
clarified signature: more types;
|
file |
diff |
annotate
|
Mon, 08 Oct 2018 17:12:28 +0200 |
Lars Hupel |
Jenkins: run ocaml_setup
|
file |
diff |
annotate
|
Thu, 07 Jun 2018 15:08:18 +0200 |
nipkow |
comments
|
file |
diff |
annotate
|
Wed, 06 Jun 2018 18:19:55 +0200 |
nipkow |
reorient -> split; documented split
|
file |
diff |
annotate
|
Thu, 26 Apr 2018 19:51:32 +0200 |
nipkow |
new simp modifier: reorient
|
file |
diff |
annotate
|
Sun, 25 Feb 2018 15:44:46 +0100 |
wenzelm |
eliminated ASCII syntax from Pure bootstrap;
|
file |
diff |
annotate
|
Sun, 18 Feb 2018 15:05:21 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Thu, 01 Feb 2018 15:31:25 +0100 |
wenzelm |
clarified signature: prefer proper order operation;
|
file |
diff |
annotate
|
Sun, 29 Oct 2017 07:46:28 +0100 |
nipkow |
reduced simp_depth_limit
|
file |
diff |
annotate
|
Tue, 13 Dec 2016 11:51:42 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
Thu, 02 Jun 2016 16:23:10 +0200 |
wenzelm |
avoid warnings on duplicate rules in the given list;
|
file |
diff |
annotate
|
Fri, 08 Apr 2016 20:15:20 +0200 |
wenzelm |
eliminated unused simproc identifier;
|
file |
diff |
annotate
|
Tue, 05 Apr 2016 20:03:24 +0200 |
wenzelm |
clarified modules -- simplified bootstrap;
|
file |
diff |
annotate
|
Mon, 31 Aug 2015 18:59:27 +0200 |
wenzelm |
routine check of theory context;
|
file |
diff |
annotate
|
Wed, 09 Sep 2015 20:57:21 +0200 |
wenzelm |
simplified simproc programming interfaces;
|
file |
diff |
annotate
|
Wed, 02 Sep 2015 23:31:41 +0200 |
wenzelm |
eliminated pointless cterms;
|
file |
diff |
annotate
|
Wed, 02 Sep 2015 22:14:44 +0200 |
wenzelm |
trim context for persistent storage;
|
file |
diff |
annotate
|
Wed, 02 Sep 2015 20:14:19 +0200 |
wenzelm |
more thorough transfer;
|
file |
diff |
annotate
|
Sun, 30 Aug 2015 21:26:42 +0200 |
wenzelm |
trim context for persistent storage;
|
file |
diff |
annotate
|
Tue, 28 Jul 2015 20:59:39 +0200 |
wenzelm |
more 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
|
Mon, 01 Jun 2015 10:47:08 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Tue, 12 May 2015 08:48:11 +0200 |
nipkow |
this warning is hardly useful but produces noisy markers in the jedit interface
|
file |
diff |
annotate
|
Fri, 13 Mar 2015 16:09:55 +0100 |
nipkow |
rhs of eqn is only eta- but not beta-eta-contracted; hence the latter is performed explicitly if needed
|
file |
diff |
annotate
|
Sat, 07 Mar 2015 21:32:31 +0100 |
wenzelm |
clarified Drule.gen_all: observe context more carefully;
|
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 22:05:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|