| Sat, 21 Oct 2023 11:24:34 +0200 |
wenzelm |
more standard simproc_setup using ML antiquotation;
|
file |
diff |
annotate
|
| Thu, 28 Oct 2021 21:28:52 +0200 |
wenzelm |
clarified antiquotations;
|
file |
diff |
annotate
|
| Sun, 24 Oct 2021 20:25:51 +0200 |
wenzelm |
clarified name, syntax, messages;
|
file |
diff |
annotate
|
| Sun, 24 Oct 2021 18:29:21 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Fri, 15 Oct 2021 19:25:31 +0200 |
wenzelm |
discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
|
file |
diff |
annotate
|
| Thu, 14 Oct 2021 16:03:20 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 02 Oct 2021 11:20:12 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 29 Sep 2021 22:54:38 +0200 |
wenzelm |
clarified antiquotations;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2021 17:20:41 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2021 14:50:26 +0200 |
wenzelm |
clarified set of items with order of addition;
|
file |
diff |
annotate
|
| Mon, 06 Sep 2021 14:05:22 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 05 Sep 2021 21:09:31 +0200 |
wenzelm |
more scalable operations;
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 01 Feb 2018 13:55:10 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Fri, 08 Apr 2016 20:15:20 +0200 |
wenzelm |
eliminated unused simproc identifier;
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:41:14 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Wed, 09 Sep 2015 20:57:21 +0200 |
wenzelm |
simplified simproc programming interfaces;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 17:25:36 +0200 |
wenzelm |
tuned -- avoid slightly odd @{cpat};
|
file |
diff |
annotate
|
| Tue, 28 Jul 2015 19:49:54 +0200 |
wenzelm |
more direct access to atomic cterms;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:39:08 +0200 |
wenzelm |
proper context for Object_Logic operations;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 22:05:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Sun, 02 Mar 2014 22:39:34 +0100 |
wenzelm |
more standard module name;
|
file |
diff |
annotate
|
| Sun, 02 Mar 2014 22:37:55 +0100 |
wenzelm |
silence warning due to addsimps @{thms dnf_simps}: duplicate not_not rule via simp_thms and nnf_simps;
|
file |
diff |
annotate
|
| Sun, 02 Mar 2014 22:24:52 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 27 Feb 2014 21:27:58 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Sat, 15 Feb 2014 18:48:43 +0100 |
wenzelm |
removed dead code;
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 23:19:30 +0100 |
wenzelm |
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
|
file |
diff |
annotate
|
| Sun, 27 Nov 2011 23:10:19 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 20:51:17 +0200 |
haftmann |
formerly unnamed infix impliciation now named HOL.implies
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 16:08:59 +0200 |
haftmann |
tuned quotes
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 11:02:14 +0200 |
haftmann |
use antiquotations for remaining unqualified constants in HOL
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
| Tue, 25 May 2010 22:21:31 +0200 |
wenzelm |
moved ML files where they are actually used;
|
file |
diff |
annotate
| base
|