| Thu, 26 Dec 2013 22:47:49 +0100 |
haftmann |
prefer ephemeral interpretation over interpretation in proof contexts;
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Fri, 15 Nov 2013 22:02:01 +0100 |
haftmann |
proper code equations for Gcd and Lcm on nat and int
|
file |
diff |
annotate
|
| Tue, 05 Nov 2013 09:44:57 +0100 |
hoelzl |
generalize SUP and INF to the syntactic type classes Sup and Inf
|
file |
diff |
annotate
|
| Thu, 25 Jul 2013 08:57:16 +0200 |
haftmann |
factored syntactic type classes for bot and top (by Alessandro Coglio)
|
file |
diff |
annotate
|
| Wed, 19 Jun 2013 17:33:51 +0200 |
noschinl |
added coprimality lemma
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 22:09:39 +0100 |
haftmann |
avoid odd foundational terms after interpretation;
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 20:50:39 +0100 |
haftmann |
fundamental revision of big operators on sets
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| Fri, 27 Jul 2012 19:57:23 +0200 |
wenzelm |
tuned proofs -- avoid odd situations of polymorphic Frees in goal state;
|
file |
diff |
annotate
|
| Tue, 27 Dec 2011 09:15:26 +0100 |
haftmann |
prefer canonical fold on lists
|
file |
diff |
annotate
|
| Thu, 27 Oct 2011 07:46:57 +0200 |
huffman |
fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
|
file |
diff |
annotate
|
| Tue, 25 Oct 2011 12:00:52 +0200 |
huffman |
merge Gcd/GCD and Lcm/LCM
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Fri, 09 Sep 2011 00:22:18 +0200 |
krauss |
added syntactic classes for "inf" and "sup"
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 09:02:58 -0700 |
huffman |
avoid using legacy theorem names
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 19:03:41 -0700 |
huffman |
avoid using legacy theorem names
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 13:55:26 +0200 |
haftmann |
observe distinction between sets and predicates more properly
|
file |
diff |
annotate
|
| Fri, 20 May 2011 11:44:16 +0200 |
haftmann |
names of fold_set locales resemble name of characteristic property more closely
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 10:44:19 +0100 |
blanchet |
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
|
file |
diff |
annotate
|
| Fri, 14 Jan 2011 15:44:47 +0100 |
wenzelm |
eliminated global prems;
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 11:39:27 +0200 |
haftmann |
avoid explicit mandatory prefix markers when prefixes are mandatory implicitly
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 11:34:19 +0200 |
haftmann |
dropped group_simps, ring_simps, field_eq_simps
|
file |
diff |
annotate
|
| Thu, 11 Mar 2010 14:39:58 +0100 |
haftmann |
tuned prefixes of ac interpretations
|
file |
diff |
annotate
|
| Mon, 08 Mar 2010 09:38:58 +0100 |
haftmann |
transfer: avoid camel case
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 14:19:53 +0100 |
haftmann |
crossproduct coprimality lemmas
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 14:21:44 -0800 |
huffman |
get rid of many duplicate simp rule warnings
|
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:43 +0100 |
haftmann |
dropped mk_left_commute; use interpretation of locale abel_semigroup instead
|
file |
diff |
annotate
|
| Sun, 10 Jan 2010 18:43:45 +0100 |
berghofe |
Adapted to changes in induct method.
|
file |
diff |
annotate
|
| Fri, 01 Jan 2010 19:15:43 +0100 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Fri, 01 Jan 2010 17:21:44 +0100 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Fri, 01 Jan 2010 16:34:51 +0100 |
nipkow |
removed FIXME
|
file |
diff |
annotate
|
| Tue, 08 Dec 2009 13:40:57 +0100 |
haftmann |
resorted code equations from "old" number theory version
|
file |
diff |
annotate
|
| Fri, 04 Dec 2009 08:52:09 +0100 |
nipkow |
removed redundant lemma
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 14:14:04 +0100 |
nipkow |
renamed lemmas "anti_sym" -> "antisym"
|
file |
diff |
annotate
|
| Thu, 29 Oct 2009 11:41:36 +0100 |
haftmann |
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 18:59:24 +0200 |
blanchet |
continuation of Nitpick's integration into Isabelle;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Tue, 06 Oct 2009 15:51:34 +0200 |
haftmann |
added syntactic Inf and Sup
|
file |
diff |
annotate
|
| Tue, 01 Sep 2009 15:39:33 +0200 |
haftmann |
some reorganization of number theory
|
file |
diff |
annotate
|
| Wed, 26 Aug 2009 19:54:01 +0200 |
nipkow |
got rid of complicated class finite_intvl_succ and defined "upto" directly on int, the only instance of the class.
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 14:08:58 +0200 |
nipkow |
Made dvd/gcd/lcm a complete lattice by introducing Gcd/GCD/Lcm/LCM
|
file |
diff |
annotate
|
| Tue, 21 Jul 2009 11:01:07 +0200 |
nipkow |
Tests for executability of "prime"
|
file |
diff |
annotate
|
| Fri, 17 Jul 2009 10:07:15 +0200 |
berghofe |
merged
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 17:18:51 +0200 |
berghofe |
merged
|
file |
diff |
annotate
|
| Fri, 10 Jul 2009 10:45:30 -0400 |
avigad |
Moved factorial lemmas from Binomial.thy to Fact.thy and merged.
|
file |
diff |
annotate
|
| Wed, 15 Jul 2009 20:34:58 +0200 |
nipkow |
Made "prime" executable
|
file |
diff |
annotate
|
| Mon, 13 Jul 2009 19:07:05 +0200 |
berghofe |
Tuned proof of lcm_1_iff_int, because metis produced enormous proof term.
|
file |
diff |
annotate
|
| Sun, 12 Jul 2009 14:48:01 +0200 |
nipkow |
more gcd/lcm lemmas
|
file |
diff |
annotate
|
| Sun, 12 Jul 2009 10:14:51 +0200 |
nipkow |
More about gcd/lcm, and some cleaning up
|
file |
diff |
annotate
|
| Tue, 07 Jul 2009 17:39:51 +0200 |
nipkow |
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
|
file |
diff |
annotate
|
| Fri, 26 Jun 2009 19:44:39 +0200 |
nipkow |
lcm abs lemmas
|
file |
diff |
annotate
|
| Fri, 26 Jun 2009 10:46:33 +0200 |
nipkow |
gcd abs lemmas
|
file |
diff |
annotate
|
| Thu, 25 Jun 2009 07:34:12 +0200 |
nipkow |
Cleaned up GCD
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 12:58:53 +0200 |
nipkow |
new lemmas
|
file |
diff |
annotate
|
| Sun, 21 Jun 2009 23:04:37 +0200 |
nipkow |
new lemmas
|
file |
diff |
annotate
|
| Sat, 20 Jun 2009 13:34:54 +0200 |
nipkow |
added lemmas; tuned
|
file |
diff |
annotate
|
| Sat, 20 Jun 2009 01:53:39 +0200 |
nipkow |
new lemmas and tuning
|
file |
diff |
annotate
|
| Thu, 18 Jun 2009 07:46:30 -0700 |
huffman |
more [code del] declarations
|
file |
diff |
annotate
|