| 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
|