| Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Sat, 28 Jul 2012 07:26:37 +0200 |
huffman |
move exception handlers outside of let block
|
file |
diff |
annotate
|
| Fri, 27 Jul 2012 19:27:21 +0200 |
huffman |
move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
|
file |
diff |
annotate
|
| Fri, 27 Jul 2012 17:59:18 +0200 |
huffman |
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
|
file |
diff |
annotate
|
| Fri, 27 Jul 2012 17:57:31 +0200 |
huffman |
give Nat_Arith simprocs proper name bindings by using simproc_setup
|
file |
diff |
annotate
|
| Fri, 20 Jul 2012 10:53:25 +0200 |
huffman |
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
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
|
| 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
|
| Tue, 09 Feb 2010 11:47:47 +0100 |
haftmann |
hide fact names clashing with fact names from Group.thy
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 17:12:27 +0100 |
haftmann |
hide fact Nat.add_0_right; make add_0_right from Groups priority
|
file |
diff |
annotate
|
| Thu, 28 Jan 2010 11:48:49 +0100 |
haftmann |
new theory Algebras.thy for generic algebraic structures
|
file |
diff |
annotate
|
| Wed, 15 Jul 2009 23:48:21 +0200 |
wenzelm |
more antiquotations;
|
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
| base
|