| Fri, 18 Dec 2009 20:13:23 -0800 |
huffman |
generalize lemma add_minus_cancel, add lemma minus_add, simplify some proofs
|
file |
diff |
annotate
|
| Fri, 18 Dec 2009 19:00:11 -0800 |
huffman |
rename equals_zero_I to minus_unique (keep old name too)
|
file |
diff |
annotate
|
| Fri, 30 Oct 2009 18:32:40 +0100 |
haftmann |
tuned code setup
|
file |
diff |
annotate
|
| Tue, 22 Sep 2009 15:36:55 +0200 |
haftmann |
be more cautious wrt. simp rules: inf_absorb1, inf_absorb2, sup_absorb1, sup_absorb2 are no simp rules by default any longer
|
file |
diff |
annotate
|
| Fri, 28 Aug 2009 19:15:59 +0200 |
nipkow |
tuned proofs
|
file |
diff |
annotate
|
| Fri, 28 Aug 2009 18:52:41 +0200 |
nipkow |
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
|
file |
diff |
annotate
|
| Mon, 20 Jul 2009 08:32:07 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 15:54:19 +0200 |
haftmann |
refinement of lattice classes
|
file |
diff |
annotate
|
| Wed, 15 Jul 2009 23:48:21 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Thu, 02 Jul 2009 17:34:14 +0200 |
wenzelm |
renamed NamedThmsFun to Named_Thms;
|
file |
diff |
annotate
|
| Mon, 04 May 2009 14:49:49 +0200 |
haftmann |
dropped duplicate lemma sum_nonneg_eq_zero_iff
|
file |
diff |
annotate
|
| Tue, 28 Apr 2009 15:50:30 +0200 |
haftmann |
lemma sum_nonneg_eq_zero_iff
|
file |
diff |
annotate
|
| Mon, 23 Mar 2009 13:26:52 -0700 |
huffman |
lemmas add_sign_intros
|
file |
diff |
annotate
|
| Sat, 21 Mar 2009 03:23:17 -0700 |
huffman |
move diff_eq_0_iff_eq into class locale context
|
file |
diff |
annotate
|
| Sat, 14 Feb 2009 16:51:18 -0800 |
huffman |
generalize lemma eq_neg_iff_add_eq_0, and move to OrderedGroup
|
file |
diff |
annotate
|
| Fri, 13 Feb 2009 14:12:00 -0800 |
huffman |
add class cancel_comm_monoid_add
|
file |
diff |
annotate
|
| Thu, 12 Feb 2009 21:24:14 -0800 |
huffman |
add lemma add_nonneg_eq_0_iff
|
file |
diff |
annotate
|
| Sun, 08 Feb 2009 11:59:26 +0100 |
nipkow |
added noatps
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 17:12:25 +0100 |
nipkow |
removed spurious conflic msg
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:57:12 +0100 |
nipkow |
merged - resolving conflics
|
file |
diff |
annotate
|
| Wed, 28 Jan 2009 16:29:16 +0100 |
nipkow |
Replaced group_ and ring_simps by algebra_simps;
|
file |
diff |
annotate
|
| Mon, 19 Jan 2009 08:16:42 +0100 |
haftmann |
tuned proof
|
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
|
| Mon, 17 Nov 2008 17:00:55 +0100 |
haftmann |
tuned unfold_locales invocation
|
file |
diff |
annotate
|
| Wed, 17 Sep 2008 21:27:08 +0200 |
wenzelm |
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
|
file |
diff |
annotate
|
| Thu, 04 Sep 2008 17:18:44 +0200 |
huffman |
move diff_add_cancel, add_diff_cancel from class ab_group_add to group_add
|
file |
diff |
annotate
|
| Thu, 10 Jul 2008 07:15:19 +0200 |
huffman |
by intro_locales -> ..
|
file |
diff |
annotate
|
| Thu, 03 Jul 2008 18:15:39 +0200 |
huffman |
move proofs of add_left_cancel and add_right_cancel into the correct locale
|
file |
diff |
annotate
|
| Wed, 18 Jun 2008 18:54:57 +0200 |
wenzelm |
simplified Abel_Cancel setup;
|
file |
diff |
annotate
|
| Sat, 29 Mar 2008 19:14:00 +0100 |
wenzelm |
replaced 'ML_setup' by 'ML';
|
file |
diff |
annotate
|
| Fri, 15 Feb 2008 16:09:10 +0100 |
haftmann |
moved *_reorient lemmas here
|
file |
diff |
annotate
|
| Wed, 30 Jan 2008 10:57:47 +0100 |
haftmann |
idempotent semigroups
|
file |
diff |
annotate
|
| Wed, 02 Jan 2008 15:14:02 +0100 |
haftmann |
splitted class uminus from class minus
|
file |
diff |
annotate
|
| Thu, 13 Dec 2007 07:09:01 +0100 |
haftmann |
dropped ws
|
file |
diff |
annotate
|
| Fri, 30 Nov 2007 20:13:06 +0100 |
haftmann |
using intro_locales instead of unfold_locales if appropriate
|
file |
diff |
annotate
|
| Tue, 06 Nov 2007 13:12:48 +0100 |
haftmann |
simplified specification of *_abs class
|
file |
diff |
annotate
|
| Tue, 06 Nov 2007 08:47:25 +0100 |
haftmann |
renamed lordered_*_* to lordered_*_add_*; further localization
|
file |
diff |
annotate
|
| Fri, 02 Nov 2007 18:52:58 +0100 |
haftmann |
proper reinitialisation after subclass
|
file |
diff |
annotate
|
| Tue, 30 Oct 2007 08:45:54 +0100 |
haftmann |
continued localization
|
file |
diff |
annotate
|
| Thu, 25 Oct 2007 19:27:52 +0200 |
haftmann |
dropped redundancy
|
file |
diff |
annotate
|
| Fri, 19 Oct 2007 19:45:29 +0200 |
haftmann |
antisymmetry not a default intro rule any longer
|
file |
diff |
annotate
|
| Fri, 19 Oct 2007 07:48:25 +0200 |
haftmann |
98% localized
|
file |
diff |
annotate
|
| Thu, 18 Oct 2007 09:20:57 +0200 |
haftmann |
continued localization
|
file |
diff |
annotate
|
| Tue, 16 Oct 2007 23:12:45 +0200 |
haftmann |
global class syntax
|
file |
diff |
annotate
|
| Sat, 29 Sep 2007 08:58:51 +0200 |
haftmann |
proper syntax during class specification
|
file |
diff |
annotate
|
| Tue, 21 Aug 2007 13:30:36 +0200 |
haftmann |
moved ordered_ab_semigroup_add to OrderedGroup.thy
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 12:52:56 +0200 |
paulson |
ATP blacklisting is now in theory data, attribute noatp
|
file |
diff |
annotate
|
| Fri, 03 Aug 2007 16:28:15 +0200 |
wenzelm |
replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
|
file |
diff |
annotate
|
| Fri, 20 Jul 2007 14:28:01 +0200 |
haftmann |
split class abs from class minus
|
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, 14 Jun 2007 18:33:31 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Fri, 01 Jun 2007 10:44:26 +0200 |
haftmann |
localized
|
file |
diff |
annotate
|
| Thu, 24 May 2007 07:27:44 +0200 |
nipkow |
Introduced new classes monoid_add and group_add
|
file |
diff |
annotate
|
| Thu, 17 May 2007 19:49:40 +0200 |
haftmann |
canonical prefixing of class constants
|
file |
diff |
annotate
|
| Thu, 17 May 2007 08:41:23 +0200 |
huffman |
remove redundant instance declaration
|
file |
diff |
annotate
|
| Thu, 29 Mar 2007 14:21:45 +0200 |
haftmann |
dropped legacy ML bindings
|
file |
diff |
annotate
|
| Tue, 20 Mar 2007 15:52:39 +0100 |
haftmann |
dropped OrderedGroup.ML
|
file |
diff |
annotate
|
| Fri, 16 Mar 2007 21:32:08 +0100 |
haftmann |
adjusted to new lattice theory developement in Lattices.thy / FixedPoint.thy
|
file |
diff |
annotate
|
| Fri, 09 Mar 2007 08:45:50 +0100 |
haftmann |
stepping towards uniform lattice theory development in HOL
|
file |
diff |
annotate
|
| Fri, 02 Mar 2007 15:43:21 +0100 |
haftmann |
now using "class"
|
file |
diff |
annotate
|