| Sun, 07 Sep 2014 09:49:01 +0200 |
haftmann |
generalized
|
file |
diff |
annotate
|
| Sat, 06 Sep 2014 20:12:32 +0200 |
haftmann |
added various facts
|
file |
diff |
annotate
|
| Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Sat, 12 Apr 2014 17:26:27 +0200 |
nipkow |
made mult_pos_pos a simp rule
|
file |
diff |
annotate
|
| Fri, 11 Apr 2014 13:36:57 +0200 |
nipkow |
made mult_nonneg_nonneg a simp rule
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 09:37:48 +0200 |
hoelzl |
field_simps: better support for negation and division, and power
|
file |
diff |
annotate
|
| Wed, 19 Mar 2014 17:06:02 +0000 |
paulson |
Some rationalisation of basic lemmas
|
file |
diff |
annotate
|
| Tue, 04 Mar 2014 16:16:05 -0800 |
huffman |
fix typo
|
file |
diff |
annotate
|
| Thu, 30 Jan 2014 16:09:03 +0100 |
haftmann |
split rules for of_bool, similar to if
|
file |
diff |
annotate
|
| Mon, 09 Dec 2013 12:22:23 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Mon, 04 Nov 2013 20:10:09 +0100 |
haftmann |
fact generalization and name consolidation
|
file |
diff |
annotate
|
| Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| Thu, 31 Oct 2013 11:44:20 +0100 |
haftmann |
generalized of_bool conversion
|
file |
diff |
annotate
|
| Fri, 18 Oct 2013 10:43:20 +0200 |
blanchet |
killed most "no_atp", to make Sledgehammer more complete
|
file |
diff |
annotate
|
| Sun, 23 Jun 2013 21:16:07 +0200 |
haftmann |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 12:20:54 +0100 |
hoelzl |
move real_isLub_unique to isLub_unique in Lubs; real_sum_of_halves to RealDef; abs_diff_less_iff to Rings
|
file |
diff |
annotate
|
| Fri, 07 Dec 2012 15:53:28 +0100 |
nipkow |
corrected nonsensical associativity of `` and dvd
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 15:19:35 -0700 |
huffman |
replace lemma realpow_two_diff with new lemma square_diff_square_factored
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 10:08:47 -0700 |
huffman |
rename real_squared_diff_one_factored to square_diff_one_factored and move to Rings.thy
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 09:52:09 -0700 |
huffman |
moved division ring stuff from Rings.thy to Fields.thy
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 11:17:13 +0200 |
haftmann |
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 10:48:37 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
| Mon, 17 May 2010 18:59:59 -0700 |
huffman |
declare add_nonneg_nonneg [simp]; remove now-redundant lemmas realpow_two_le_order(2)
|
file |
diff |
annotate
|
| Mon, 17 May 2010 08:45:46 -0700 |
huffman |
remove simp attribute from square_eq_1_iff
|
file |
diff |
annotate
|
| Mon, 10 May 2010 21:27:52 -0700 |
huffman |
move lemma real_mult_is_one to Rings.thy, renamed to square_eq_1_iff
|
file |
diff |
annotate
|
| Thu, 06 May 2010 23:11:56 +0200 |
haftmann |
moved some lemmas from Groebner_Basis here
|
file |
diff |
annotate
|
| Tue, 20 Apr 2010 17:58:34 +0200 |
hoelzl |
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 11:34:15 +0200 |
haftmann |
dropped group_simps, ring_simps, field_eq_simps; classes division_ring_inverse_zero, field_inverse_zero, linordered_field_inverse_zero
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 15:17:59 +0200 |
haftmann |
less special treatment of times_divide_eq [simp]
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 13:58:14 +0200 |
haftmann |
more localization; factored out lemmas for division_ring
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 12:58:52 +0100 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file |
diff |
annotate
|
| Sat, 06 Mar 2010 18:24:30 -0800 |
huffman |
generalize some lemmas from class linordered_ring_strict to linordered_ring
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 15:53:18 +0100 |
haftmann |
tuned text
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 14:21:44 -0800 |
huffman |
get rid of many duplicate simp rule warnings
|
file |
diff |
annotate
|
| Wed, 10 Feb 2010 15:52:12 +0100 |
haftmann |
dropped last occurence of the linlinordered accident
|
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
|
| Wed, 10 Feb 2010 08:49:26 +0100 |
haftmann |
division ring assumes divide_inverse
|
file |
diff |
annotate
|
| Mon, 08 Feb 2010 17:12:38 +0100 |
haftmann |
renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
|
file |
diff |
annotate
| base
|