| Fri, 13 May 2011 23:58:40 +0200 |
wenzelm |
clarified map_simpset versus Simplifier.map_simpset_global;
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 20:42:09 +0200 |
wenzelm |
Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 18:36:22 +0200 |
wenzelm |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 21:50:05 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
file |
diff |
annotate
|
| Fri, 19 Feb 2010 14:47:01 +0100 |
haftmann |
moved remaning class operations from Algebras.thy to Groups.thy
|
file |
diff |
annotate
|
| Wed, 10 Feb 2010 14:12:04 +0100 |
haftmann |
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
|
file |
diff |
annotate
|
| Fri, 05 Feb 2010 14:33:50 +0100 |
haftmann |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file |
diff |
annotate
|
| Thu, 28 Jan 2010 11:48:49 +0100 |
haftmann |
new theory Algebras.thy for generic algebraic structures
|
file |
diff |
annotate
|
| Wed, 28 Oct 2009 19:09:47 +0100 |
haftmann |
moved theory Divides after theory Nat_Numeral; tuned some proof texts
|
file |
diff |
annotate
|
| Fri, 18 Sep 2009 09:07:50 +0200 |
haftmann |
tuned const_name antiquotations
|
file |
diff |
annotate
|
| Mon, 08 Jun 2009 22:29:37 +0200 |
boehmes |
fast_lin_arith uses proper multiplication instead of unfolding to additions
|
file |
diff |
annotate
|
| Mon, 11 May 2009 15:57:29 +0200 |
haftmann |
qualified names for Lin_Arith tactics and simprocs
|
file |
diff |
annotate
|
| Mon, 11 May 2009 15:18:32 +0200 |
haftmann |
tuned interface of Lin_Arith
|
file |
diff |
annotate
|
| Sat, 09 May 2009 09:17:29 +0200 |
haftmann |
interface changes in linarith.ML
|
file |
diff |
annotate
|
| Fri, 08 May 2009 09:48:07 +0200 |
haftmann |
modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
|
file |
diff |
annotate
|
| Wed, 29 Apr 2009 17:15:01 -0700 |
huffman |
reimplement reorientation simproc using theory data
|
file |
diff |
annotate
|
| Mon, 30 Mar 2009 12:07:59 -0700 |
huffman |
simplify theorem references
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 11:33:50 -0700 |
huffman |
parameterize assoc_fold with is_numeral predicate
|
file |
diff |
annotate
|
| Mon, 23 Mar 2009 19:01:15 +0100 |
haftmann |
structure LinArith now named Lin_Arith
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 19:17:57 +0100 |
haftmann |
moved some generic nonsense to arith_data.ML
|
file |
diff |
annotate
|
| Thu, 12 Mar 2009 18:01:26 +0100 |
haftmann |
vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
|
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, 03 Dec 2008 15:58:44 +0100 |
haftmann |
made repository layout more coherent with logical distribution structure; stripped some $Id$s
|
file |
diff |
annotate
| base
|