| Thu, 14 Oct 2021 16:03:20 +0200 |
wenzelm |
clarified signature;
|
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, 13 Apr 2019 22:06:40 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 13 Apr 2019 21:51:24 +0200 |
wenzelm |
prefer ctyp operations;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
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, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Thu, 31 Oct 2013 11:44:20 +0100 |
haftmann |
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
|
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
|
| Sun, 27 Nov 2011 23:10:19 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Fri, 07 Jan 2011 22:44:07 +0100 |
wenzelm |
do not open ML structures;
|
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
|
| Sat, 15 May 2010 21:50:05 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
file |
diff |
annotate
|
| Sun, 28 Feb 2010 23:51:31 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Fri, 18 Sep 2009 09:07:50 +0200 |
haftmann |
tuned const_name antiquotations
|
file |
diff |
annotate
|
| Sun, 22 Mar 2009 20:46:12 +0100 |
haftmann |
more antiquotations
|
file |
diff |
annotate
|
| Sun, 22 Jul 2007 17:53:50 +0200 |
chaieb |
tuned
|
file |
diff |
annotate
|
| Thu, 19 Jul 2007 21:47:42 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 20:01:30 +0200 |
wenzelm |
renamed Conv.is_refl to Thm.is_reflexive;
|
file |
diff |
annotate
|
| Mon, 02 Jul 2007 10:43:20 +0200 |
chaieb |
Generic QE need no Context anymore
|
file |
diff |
annotate
|
| Mon, 25 Jun 2007 00:36:38 +0200 |
wenzelm |
made type conv pervasive;
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 20:48:48 +0200 |
wenzelm |
moved quantifier elimination tools to Tools/Qelim/;
|
file |
diff |
annotate
|