| Fri, 28 Mar 2008 19:43:54 +0100 |
wenzelm |
avoid rebinding of existing facts;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2008 20:33:28 +0100 |
wenzelm |
avoid rebinding of existing facts;
|
file |
diff |
annotate
|
| Wed, 27 Feb 2008 14:39:48 +0100 |
chaieb |
Installation of Quantifier elimination for ordered fields moved to Library/Dense_Linear_Order.thy
|
file |
diff |
annotate
|
| Tue, 15 Jan 2008 16:19:23 +0100 |
haftmann |
joined theories IntDef, Numeral, IntArith to theory Int
|
file |
diff |
annotate
|
| Wed, 28 Nov 2007 09:01:34 +0100 |
haftmann |
dropped legacy ml bindings
|
file |
diff |
annotate
|
| Wed, 31 Oct 2007 12:19:33 +0100 |
chaieb |
exported field_comp_conv: a numerical conversion over fields
|
file |
diff |
annotate
|
| Sun, 21 Oct 2007 12:33:12 +0200 |
chaieb |
Fixed Bug in instantiation of Groebner Bases to field: dest_const used to raise TERM where the tactic handles ERROR
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 12:52:56 +0200 |
paulson |
ATP blacklisting is now in theory data, attribute noatp
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 00:56:26 +0200 |
wenzelm |
arith method setup: proper context;
|
file |
diff |
annotate
|
| Sun, 22 Jul 2007 17:53:42 +0200 |
chaieb |
Tunes Proof
|
file |
diff |
annotate
|
| Fri, 20 Jul 2007 14:28:25 +0200 |
haftmann |
moved class ord from Orderings.thy to HOL.thy
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 00:06:09 +0200 |
wenzelm |
Numeral.mk_cnumber;
|
file |
diff |
annotate
|
| Sat, 23 Jun 2007 19:33:22 +0200 |
nipkow |
tuned and renamed group_eq_simps and ring_eq_simps
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 20:48:47 +0200 |
wenzelm |
moved Presburger setup back to Presburger.thy;
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 17:28:50 +0200 |
wenzelm |
renamed NatSimprocs.thy to Arith_Tools.thy;
|
file |
diff |
annotate
|