| Wed, 24 Jun 2009 09:41:14 +0200 |
nipkow |
corrected and unified thm names
|
file |
diff |
annotate
|
| Thu, 16 Apr 2009 14:02:13 +0200 |
haftmann |
added simproc
|
file |
diff |
annotate
|
| Tue, 24 Mar 2009 13:13:18 +0100 |
nipkow |
fix
|
file |
diff |
annotate
|
| Tue, 24 Mar 2009 12:45:01 +0100 |
nipkow |
presburger uses [arith] now
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
| Tue, 03 Mar 2009 17:05:18 +0100 |
nipkow |
removed and renamed redundant lemmas
|
file |
diff |
annotate
|
| Sat, 21 Feb 2009 20:52:30 +0100 |
nipkow |
Removed subsumed lemmas
|
file |
diff |
annotate
|
| Sat, 21 Feb 2009 09:58:26 +0100 |
nipkow |
removed redundant thms
|
file |
diff |
annotate
|
| Fri, 20 Feb 2009 23:46:03 +0100 |
nipkow |
Removed redundant lemmas
|
file |
diff |
annotate
|
| Tue, 17 Feb 2009 20:42:19 +0000 |
chaieb |
merged
|
file |
diff |
annotate
|
| Tue, 17 Feb 2009 20:41:36 +0000 |
chaieb |
fixed selection of premises
|
file |
diff |
annotate
|
| Tue, 17 Feb 2009 18:48:17 +0100 |
nipkow |
Cleaned up IntDiv and removed subsumed lemmas.
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 15:30:10 +0100 |
wenzelm |
moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 00:08:13 +0100 |
wenzelm |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
file |
diff |
annotate
|
| Thu, 18 Sep 2008 19:39:44 +0200 |
wenzelm |
simplified oracle interface;
|
file |
diff |
annotate
|
| Fri, 18 Jul 2008 18:25:53 +0200 |
haftmann |
moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
|
file |
diff |
annotate
|
| Thu, 29 May 2008 23:46:40 +0200 |
wenzelm |
proper context for ss;
|
file |
diff |
annotate
|
| Sat, 05 Jan 2008 23:05:29 +0100 |
chaieb |
Tuned relevant premises selection
|
file |
diff |
annotate
|
| Thu, 03 Jan 2008 18:19:27 +0100 |
chaieb |
tuned relevance test for presburger
|
file |
diff |
annotate
|
| Thu, 03 Jan 2008 10:27:34 +0100 |
chaieb |
Changed order of tactics in presburger --- thinning before case splits
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 15:14:24 +0100 |
haftmann |
some more antiquotations
|
file |
diff |
annotate
|
| Fri, 12 Oct 2007 08:25:48 +0200 |
haftmann |
moved class power to theory Power
|
file |
diff |
annotate
|
| Sat, 15 Sep 2007 19:27:35 +0200 |
haftmann |
fixed title
|
file |
diff |
annotate
|
| Wed, 22 Aug 2007 17:13:41 +0200 |
chaieb |
More selective generalization : a*b is generalized whenever none of a and b is a number
|
file |
diff |
annotate
|
| Fri, 20 Jul 2007 14:28:05 +0200 |
haftmann |
dropped Nat.ML legacy bindings
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 17:17:04 +0200 |
wenzelm |
CONVERSION tactical;
|
file |
diff |
annotate
|
| Mon, 25 Jun 2007 22:46:55 +0200 |
wenzelm |
tactics: more robust addressing of subgoal using (C)SUBGOAL/THEN_ALL_NEW;
|
file |
diff |
annotate
|
| Mon, 25 Jun 2007 00:36:37 +0200 |
wenzelm |
Thm.eta_long_conversion;
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 22:52:22 +0200 |
huffman |
add thm antiquotations
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 20:48:48 +0200 |
wenzelm |
moved quantifier elimination tools to Tools/Qelim/;
|
file |
diff |
annotate
|