| Mon, 23 Mar 2009 19:01:16 +0100 |
haftmann |
moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
|
file |
diff |
annotate
|
| Thu, 19 Mar 2009 22:05:00 +0100 |
wenzelm |
proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
|
file |
diff |
annotate
|
| Wed, 11 Mar 2009 15:56:50 +0100 |
haftmann |
tuned funny error message
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 08:23:11 +0100 |
haftmann |
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
|
file |
diff |
annotate
|
| Tue, 03 Feb 2009 16:50:40 +0100 |
haftmann |
regenerated presburger code
|
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
|
| Mon, 29 Sep 2008 11:46:47 +0200 |
wenzelm |
handle _ should be avoided (spurious Interrupt will spoil the game);
|
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
|
| Mon, 23 Jun 2008 23:45:39 +0200 |
wenzelm |
Logic.all/mk_equals/mk_implies;
|
file |
diff |
annotate
|
| Thu, 29 May 2008 23:46:39 +0200 |
wenzelm |
proper context for simp_thms_conv;
|
file |
diff |
annotate
|
| Sat, 17 May 2008 13:54:30 +0200 |
wenzelm |
structure Display: less pervasive operations;
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 15:14:24 +0100 |
haftmann |
some more antiquotations
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 16:08:00 +0200 |
wenzelm |
simplified type int (eliminated IntInf.int, integer);
|
file |
diff |
annotate
|
| Sat, 15 Sep 2007 19:27:35 +0200 |
haftmann |
fixed title
|
file |
diff |
annotate
|
| Thu, 16 Aug 2007 21:52:07 +0200 |
wenzelm |
removed dead code;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 00:56:26 +0200 |
wenzelm |
arith method setup: proper context;
|
file |
diff |
annotate
|
| Fri, 20 Jul 2007 14:28:25 +0200 |
haftmann |
moved class ord from Orderings.thy to HOL.thy
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 17:30:54 +0200 |
haftmann |
now works with SML/NJ
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 09:23:15 +0200 |
haftmann |
replaced code generator framework for reflected cooper
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 00:06:20 +0200 |
wenzelm |
avoid polymorphic equality;
|
file |
diff |
annotate
|
| Mon, 02 Jul 2007 10:43:19 +0200 |
chaieb |
Handle exception TYPE
|
file |
diff |
annotate
|
| Fri, 29 Jun 2007 21:23:05 +0200 |
haftmann |
tuned arithmetic modules
|
file |
diff |
annotate
|
| Thu, 28 Jun 2007 19:09:36 +0200 |
haftmann |
dropped Library.lcm
|
file |
diff |
annotate
|
| Mon, 25 Jun 2007 00:36:33 +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
|