Tue, 02 May 2006 20:42:30 +0200 |
wenzelm |
replaced syntax/translations by abbreviation;
|
file |
diff |
annotate
|
Sat, 08 Apr 2006 22:51:06 +0200 |
wenzelm |
refined 'abbreviation';
|
file |
diff |
annotate
|
Wed, 22 Mar 2006 11:14:58 +0100 |
nipkow |
translations -> abbreviations (a cool feature)
|
file |
diff |
annotate
|
Fri, 17 Mar 2006 10:04:27 +0100 |
ballarin |
Renamed setsum_mult to setsum_right_distrib.
|
file |
diff |
annotate
|
Thu, 22 Dec 2005 17:57:09 +0100 |
nipkow |
more lemmas
|
file |
diff |
annotate
|
Fri, 16 Dec 2005 16:59:32 +0100 |
nipkow |
new lemmas
|
file |
diff |
annotate
|
Fri, 07 Oct 2005 22:59:19 +0200 |
wenzelm |
replaced _K by dummy abstraction;
|
file |
diff |
annotate
|
Tue, 04 Oct 2005 23:30:46 +0200 |
nipkow |
new lemmas
|
file |
diff |
annotate
|
Thu, 22 Sep 2005 23:56:15 +0200 |
nipkow |
renamed rules to iprover
|
file |
diff |
annotate
|
Tue, 30 Aug 2005 12:47:53 +0200 |
paulson |
patterns in setsum and setprod
|
file |
diff |
annotate
|
Fri, 26 Aug 2005 10:01:06 +0200 |
ballarin |
Lemmas on dvd, power and finite summation added or strengthened.
|
file |
diff |
annotate
|
Tue, 16 Aug 2005 18:53:11 +0200 |
paulson |
more simprules now have names
|
file |
diff |
annotate
|
Fri, 05 Aug 2005 12:20:30 +0200 |
nipkow |
added Brian Hufmann's finite instances
|
file |
diff |
annotate
|
Tue, 12 Jul 2005 17:56:03 +0200 |
avigad |
added lemmas to OrderedGroup.thy (reasoning about signs, absolute value, triangle inequalities)
|
file |
diff |
annotate
|
Fri, 08 Jul 2005 11:38:30 +0200 |
nipkow |
changed imports due to new GCD.thy
|
file |
diff |
annotate
|
Thu, 07 Jul 2005 12:39:17 +0200 |
nipkow |
linear arithmetic now takes "&" in assumptions apart.
|
file |
diff |
annotate
|
Fri, 01 Jul 2005 13:51:11 +0200 |
berghofe |
Added strong_setsum_cong and strong_setprod_cong.
|
file |
diff |
annotate
|
Thu, 23 Jun 2005 19:40:03 +0200 |
nipkow |
fixed \<Prod> syntax
|
file |
diff |
annotate
|
Mon, 25 Apr 2005 17:58:41 +0200 |
ballarin |
Subsumption of locale interpretations.
|
file |
diff |
annotate
|
Thu, 21 Apr 2005 17:22:17 +0200 |
nipkow |
tuning locales
|
file |
diff |
annotate
|
Wed, 20 Apr 2005 17:19:18 +0200 |
nipkow |
Used locale interpretations everywhere.
|
file |
diff |
annotate
|
Tue, 19 Apr 2005 11:40:23 +0200 |
paulson |
fixed presentation
|
file |
diff |
annotate
|
Mon, 18 Apr 2005 15:53:51 +0200 |
ballarin |
Cleaned up, now uses interpretation.
|
file |
diff |
annotate
|
Tue, 01 Mar 2005 18:48:52 +0100 |
nipkow |
integrated Jeremy's FiniteLib
|
file |
diff |
annotate
|
Mon, 28 Feb 2005 18:29:55 +0100 |
obua |
added setsum_diff1' which holds in more general cases than setsum_diff1
|
file |
diff |
annotate
|
Tue, 22 Feb 2005 10:54:30 +0100 |
nipkow |
more setsum tuning
|
file |
diff |
annotate
|
Mon, 21 Feb 2005 19:23:46 +0100 |
nipkow |
more fine tuniung
|
file |
diff |
annotate
|
Mon, 21 Feb 2005 15:04:10 +0100 |
nipkow |
comprehensive cleanup, replacing sumr by setsum
|
file |
diff |
annotate
|
Fri, 18 Feb 2005 11:48:42 +0100 |
nipkow |
tuning
|
file |
diff |
annotate
|
Mon, 14 Feb 2005 10:24:58 +0100 |
paulson |
simplified a proof
|
file |
diff |
annotate
|
Thu, 10 Feb 2005 19:14:35 +0100 |
nipkow |
some stuff is now redundant.
|
file |
diff |
annotate
|
Thu, 10 Feb 2005 16:03:18 +0100 |
paulson |
non-inductive fold1Set proofs
|
file |
diff |
annotate
|
Thu, 10 Feb 2005 13:01:46 +0100 |
paulson |
simplified a key lemma for foldSet
|
file |
diff |
annotate
|
Thu, 10 Feb 2005 10:43:57 +0100 |
berghofe |
Subscripts for theorem lists now start at 1.
|
file |
diff |
annotate
|
Wed, 09 Feb 2005 18:50:09 +0100 |
nipkow |
Extracted generic lattice stuff to new Lattice_Locales.thy
|
file |
diff |
annotate
|
Wed, 09 Feb 2005 18:32:28 +0100 |
paulson |
new foldSet proofs
|
file |
diff |
annotate
|
Wed, 09 Feb 2005 12:08:46 +0100 |
paulson |
revised fold1 proofs
|
file |
diff |
annotate
|
Wed, 09 Feb 2005 10:17:09 +0100 |
paulson |
revised fold1 proofs
|
file |
diff |
annotate
|
Tue, 08 Feb 2005 18:32:34 +0100 |
nipkow |
cvs merge problem fixed
|
file |
diff |
annotate
|
Tue, 08 Feb 2005 15:11:30 +0100 |
paulson |
new treatment of fold1
|
file |
diff |
annotate
|
Tue, 08 Feb 2005 09:46:00 +0100 |
nipkow |
Fixed lattice defns
|
file |
diff |
annotate
|
Mon, 07 Feb 2005 18:20:46 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
Mon, 07 Feb 2005 08:02:14 +0100 |
nipkow |
fixed latex problems
|
file |
diff |
annotate
|
Sat, 05 Feb 2005 19:24:11 +0100 |
nipkow |
Added Lattice locale
|
file |
diff |
annotate
|
Fri, 04 Feb 2005 18:34:34 +0100 |
paulson |
comment
|
file |
diff |
annotate
|
Fri, 04 Feb 2005 17:14:42 +0100 |
nipkow |
Added semi-lattice locales and reorganized fold1 lemmas
|
file |
diff |
annotate
|
Wed, 02 Feb 2005 18:06:00 +0100 |
paulson |
generalization and tidying
|
file |
diff |
annotate
|
Wed, 02 Feb 2005 09:15:40 +0100 |
nipkow |
fold and fol1 changes
|
file |
diff |
annotate
|
Wed, 02 Feb 2005 08:53:03 +0100 |
nipkow |
added [simp]
|
file |
diff |
annotate
|
Sun, 30 Jan 2005 20:48:50 +0100 |
nipkow |
renamed a few vars, added a lemma
|
file |
diff |
annotate
|
Fri, 28 Jan 2005 15:44:03 +0100 |
nipkow |
proof simpification
|
file |
diff |
annotate
|
Fri, 21 Jan 2005 13:52:09 +0100 |
paulson |
new theorem image_eq_fold
|
file |
diff |
annotate
|
Tue, 14 Dec 2004 10:45:16 +0100 |
paulson |
new and stronger lemmas and improved simplification for finite sets
|
file |
diff |
annotate
|
Sun, 12 Dec 2004 16:25:47 +0100 |
nipkow |
REorganized Finite_Set
|
file |
diff |
annotate
|
Thu, 09 Dec 2004 18:30:59 +0100 |
nipkow |
First step in reorganizing Finite_Set
|
file |
diff |
annotate
|
Mon, 06 Dec 2004 14:14:03 +0100 |
nipkow |
Started to clean up and generalize FiniteSet
|
file |
diff |
annotate
|
Wed, 24 Nov 2004 11:12:10 +0100 |
nipkow |
changed the order of !!-quantifiers in finite set induction.
|
file |
diff |
annotate
|
Tue, 23 Nov 2004 18:58:59 +0100 |
obua |
prettier proof of setsum_diff
|
file |
diff |
annotate
|
Tue, 23 Nov 2004 16:42:54 +0100 |
nipkow |
renamed 2 lemmas
|
file |
diff |
annotate
|
Tue, 23 Nov 2004 15:50:27 +0100 |
obua |
relaxed type constraints of lemmas: setsum_nonneg, setsum_nonpos, setsum_negf, setsum_Un_ring
|
file |
diff |
annotate
|
Tue, 23 Nov 2004 15:25:39 +0100 |
obua |
Added lemmas setsum_mono, finite_setsum_diff1, finite_setsum_diff
|
file |
diff |
annotate
|
Tue, 23 Nov 2004 09:08:35 +0100 |
nipkow |
generalized lemma
|
file |
diff |
annotate
|
Tue, 23 Nov 2004 08:58:32 +0100 |
nipkow |
added lemma
|
file |
diff |
annotate
|
Sat, 13 Nov 2004 07:47:34 +0100 |
nipkow |
More lemmas
|
file |
diff |
annotate
|
Thu, 07 Oct 2004 15:42:30 +0200 |
paulson |
simplification tweaks for better arithmetic reasoning
|
file |
diff |
annotate
|
Mon, 04 Oct 2004 15:28:03 +0200 |
paulson |
revised simprules for division
|
file |
diff |
annotate
|
Wed, 18 Aug 2004 11:09:40 +0200 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
Mon, 16 Aug 2004 14:22:27 +0200 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
Mon, 09 Aug 2004 10:09:44 +0200 |
nipkow |
Aded a thm.
|
file |
diff |
annotate
|
Wed, 04 Aug 2004 19:11:02 +0200 |
nipkow |
added some inj_on thms
|
file |
diff |
annotate
|
Thu, 22 Jul 2004 17:37:31 +0200 |
nipkow |
Modified \<Sum> syntax a little.
|
file |
diff |
annotate
|
Thu, 15 Jul 2004 15:32:32 +0200 |
paulson |
redefining sumr to be a translation to setsum
|
file |
diff |
annotate
|
Wed, 14 Jul 2004 10:25:03 +0200 |
nipkow |
added {0::nat..n(} = {..n(}
|
file |
diff |
annotate
|
Thu, 24 Jun 2004 17:52:55 +0200 |
paulson |
ringpower to recpower
|
file |
diff |
annotate
|
Tue, 15 Jun 2004 10:40:05 +0200 |
paulson |
strengthened some theorems
|
file |
diff |
annotate
|
Wed, 09 Jun 2004 11:18:51 +0200 |
paulson |
moved some cardinality results into main HOL
|
file |
diff |
annotate
|
Fri, 14 May 2004 16:52:53 +0200 |
paulson |
removed a premise of card_inj_on_le
|
file |
diff |
annotate
|
Wed, 12 May 2004 10:00:56 +0200 |
nipkow |
fixed latex problems
|
file |
diff |
annotate
|
Tue, 11 May 2004 20:11:08 +0200 |
obua |
changes made due to new Ring_and_Field theory
|
file |
diff |
annotate
|
Fri, 23 Apr 2004 20:48:28 +0200 |
wenzelm |
tuned notation;
|
file |
diff |
annotate
|
Wed, 14 Apr 2004 14:13:05 +0200 |
kleing |
use more symbols in HTML output
|
file |
diff |
annotate
|
Thu, 01 Apr 2004 10:54:32 +0200 |
paulson |
new type class abelian_group
|
file |
diff |
annotate
|
Thu, 25 Mar 2004 10:32:21 +0100 |
paulson |
new material from Avigad
|
file |
diff |
annotate
|
Wed, 10 Mar 2004 10:34:49 +0100 |
paulson |
strengthened the axclass claims
|
file |
diff |
annotate
|
Mon, 08 Mar 2004 11:12:06 +0100 |
paulson |
generic theorems about exponentials; general tidying up
|
file |
diff |
annotate
|
Thu, 04 Mar 2004 12:06:07 +0100 |
paulson |
new material from Avigad, and simplified treatment of division by 0
|
file |
diff |
annotate
|
Sat, 27 Dec 2003 21:02:14 +0100 |
paulson |
re-organized numeric lemmas
|
file |
diff |
annotate
|
Fri, 19 Dec 2003 04:28:45 +0100 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
Fri, 26 Sep 2003 10:34:57 +0200 |
paulson |
misc tidying
|
file |
diff |
annotate
|
Thu, 20 Feb 2003 11:10:24 +0100 |
paulson |
new inverse image lemmas
|
file |
diff |
annotate
|
Fri, 29 Nov 2002 09:48:28 +0100 |
nipkow |
added a few lemmas
|
file |
diff |
annotate
|
Thu, 28 Nov 2002 10:50:42 +0100 |
ballarin |
HOL-Algebra partially ported to Isar.
|
file |
diff |
annotate
|
Wed, 13 Nov 2002 15:24:42 +0100 |
berghofe |
Transitive closure is now defined inductively as well.
|
file |
diff |
annotate
|
Fri, 27 Sep 2002 16:44:50 +0200 |
paulson |
Proof tidying
|
file |
diff |
annotate
|
Fri, 20 Sep 2002 11:48:35 +0200 |
paulson |
less use of x-symbols
|
file |
diff |
annotate
|
Mon, 12 Aug 2002 17:48:15 +0200 |
nipkow |
Added Mi and Max on sets, hid Min and Pls on numerals.
|
file |
diff |
annotate
|
Wed, 24 Jul 2002 22:15:55 +0200 |
wenzelm |
simplified locale predicates;
|
file |
diff |
annotate
|
Fri, 19 Jul 2002 18:44:36 +0200 |
wenzelm |
accomodate cumulative locale predicates;
|
file |
diff |
annotate
|
Thu, 18 Jul 2002 12:08:45 +0200 |
wenzelm |
ACe_axioms;
|
file |
diff |
annotate
|
Tue, 16 Jul 2002 18:26:09 +0200 |
wenzelm |
adapted to locale defs;
|
file |
diff |
annotate
|
Mon, 25 Feb 2002 20:48:14 +0100 |
wenzelm |
clarified syntax of ``long'' statements: fixes/assumes/shows;
|
file |
diff |
annotate
|
Fri, 11 Jan 2002 14:44:58 +0100 |
wenzelm |
lemmas (in ACe) AC;
|
file |
diff |
annotate
|
Thu, 10 Jan 2002 01:10:58 +0100 |
wenzelm |
qualified exports from locales;
|
file |
diff |
annotate
|
Thu, 06 Dec 2001 00:38:55 +0100 |
wenzelm |
renamed theory Finite to Finite_Set and converted;
|
file |
diff |
annotate
|