| Fri, 28 Mar 2008 22:00:59 +0100 |
haftmann |
only invoke interpret
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 19:04:35 +0100 |
haftmann |
no "attach UNIV" any more
|
file |
diff |
annotate
|
| Tue, 26 Feb 2008 20:38:10 +0100 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Wed, 06 Feb 2008 08:34:32 +0100 |
haftmann |
locales ACf, ACIf, ACIfSL and ACIfSLlin have been abandoned in favour of the existing algebraic classes ab_semigroup_mult, ab_semigroup_idem_mult, lower_semilattice (resp. uper_semilattice) and linorder
|
file |
diff |
annotate
|
| Fri, 07 Dec 2007 15:07:59 +0100 |
haftmann |
instantiation target rather than legacy instance
|
file |
diff |
annotate
|
| Thu, 29 Nov 2007 17:08:26 +0100 |
haftmann |
instance command as rudimentary class target
|
file |
diff |
annotate
|
| Fri, 23 Nov 2007 21:09:32 +0100 |
haftmann |
deleted card definition as code lemma; authentic syntax for card
|
file |
diff |
annotate
|
| Tue, 06 Nov 2007 08:47:25 +0100 |
haftmann |
renamed lordered_*_* to lordered_*_add_*; further localization
|
file |
diff |
annotate
|
| Fri, 26 Oct 2007 21:22:16 +0200 |
haftmann |
dropped "brown" syntax
|
file |
diff |
annotate
|
| Tue, 23 Oct 2007 23:27:23 +0200 |
nipkow |
went back to >0
|
file |
diff |
annotate
|
| Tue, 16 Oct 2007 23:12:45 +0200 |
haftmann |
global class syntax
|
file |
diff |
annotate
|
| Mon, 15 Oct 2007 15:29:39 +0200 |
haftmann |
explicit parameter for class finite
|
file |
diff |
annotate
|
| Mon, 08 Oct 2007 08:04:26 +0200 |
haftmann |
clarified
|
file |
diff |
annotate
|
| Fri, 05 Oct 2007 08:38:09 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Sat, 29 Sep 2007 08:58:51 +0200 |
haftmann |
proper syntax during class specification
|
file |
diff |
annotate
|
| Wed, 26 Sep 2007 20:27:55 +0200 |
haftmann |
moved Finite_Set before Datatype
|
file |
diff |
annotate
|
| Thu, 20 Sep 2007 16:37:28 +0200 |
haftmann |
code lemmas for cardinality
|
file |
diff |
annotate
|
| Sat, 15 Sep 2007 19:27:41 +0200 |
haftmann |
added lemmas for finiteness
|
file |
diff |
annotate
|
| Fri, 24 Aug 2007 14:21:33 +0200 |
paulson |
revised blacklisting for ATP linkup
|
file |
diff |
annotate
|
| Tue, 21 Aug 2007 13:30:36 +0200 |
haftmann |
moved ordered_ab_semigroup_add to OrderedGroup.thy
|
file |
diff |
annotate
|
| Mon, 20 Aug 2007 18:07:25 +0200 |
haftmann |
conciliated Inf/Inf_fin
|
file |
diff |
annotate
|
| Fri, 17 Aug 2007 13:58:57 +0200 |
haftmann |
dropped junk
|
file |
diff |
annotate
|
| Wed, 15 Aug 2007 12:52:56 +0200 |
paulson |
ATP blacklisting is now in theory data, attribute noatp
|
file |
diff |
annotate
|
| Tue, 14 Aug 2007 23:04:27 +0200 |
huffman |
minimize imports
|
file |
diff |
annotate
|
| Tue, 14 Aug 2007 23:03:42 +0200 |
huffman |
rename lemmas finite->finite_UNIV, finite_set->finite; declare finite[simp]
|
file |
diff |
annotate
|
| Thu, 09 Aug 2007 15:52:42 +0200 |
haftmann |
re-eliminated Option.thy
|
file |
diff |
annotate
|
| Tue, 07 Aug 2007 09:38:46 +0200 |
haftmann |
simplified proofs
|
file |
diff |
annotate
|
| Tue, 24 Jul 2007 15:20:47 +0200 |
haftmann |
using interpretation with derived concepts
|
file |
diff |
annotate
|
| Fri, 20 Jul 2007 14:27:56 +0200 |
haftmann |
simplified HOL bootstrap
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:00:46 +0200 |
berghofe |
Renamed inductive2 to inductive.
|
file |
diff |
annotate
|
| Tue, 10 Jul 2007 17:30:45 +0200 |
haftmann |
moved some finite lemmas here
|
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
|
| Sun, 17 Jun 2007 18:47:03 +0200 |
nipkow |
tuned laws for cancellation in divisions for fields.
|
file |
diff |
annotate
|
| Fri, 15 Jun 2007 15:10:32 +0200 |
nipkow |
made divide_self a simp rule
|
file |
diff |
annotate
|
| Thu, 14 Jun 2007 18:33:31 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Wed, 06 Jun 2007 17:01:33 +0200 |
huffman |
generalize class constraints on some lemmas
|
file |
diff |
annotate
|
| Mon, 04 Jun 2007 15:43:30 +0200 |
haftmann |
tuned comments
|
file |
diff |
annotate
|
| Thu, 24 May 2007 08:37:39 +0200 |
haftmann |
rudimentary class target implementation
|
file |
diff |
annotate
|
| Sat, 19 May 2007 11:33:22 +0200 |
haftmann |
no special treatment in naming of locale predicates stemming form classes
|
file |
diff |
annotate
|
| Fri, 11 May 2007 20:47:30 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Fri, 11 May 2007 03:31:12 +0200 |
huffman |
generalize setsum lemmas from semiring_0_cancel to semiring_0
|
file |
diff |
annotate
|
| Thu, 10 May 2007 10:21:46 +0200 |
haftmann |
localized Min/Max
|
file |
diff |
annotate
|
| Mon, 09 Apr 2007 21:28:24 +0200 |
huffman |
generalized type of lemma setsum_product
|
file |
diff |
annotate
|
| Tue, 20 Mar 2007 08:27:15 +0100 |
haftmann |
explizit "type" superclass
|
file |
diff |
annotate
|
| Fri, 16 Mar 2007 21:32:07 +0100 |
haftmann |
added FIXME hints
|
file |
diff |
annotate
|
| Fri, 09 Mar 2007 08:45:57 +0100 |
haftmann |
moved order on functions here
|
file |
diff |
annotate
|
| Sat, 03 Mar 2007 09:26:58 +0100 |
haftmann |
moved instance option :: finite here
|
file |
diff |
annotate
|
| Fri, 02 Mar 2007 15:43:19 +0100 |
haftmann |
added code theorems for UNIV
|
file |
diff |
annotate
|
| Wed, 14 Feb 2007 10:06:12 +0100 |
haftmann |
added class "preorder"
|
file |
diff |
annotate
|
| Wed, 07 Feb 2007 17:28:09 +0100 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
| Sun, 10 Dec 2006 07:12:26 +0100 |
nipkow |
Modified lattice locale
|
file |
diff |
annotate
|
| Sat, 02 Dec 2006 11:33:08 +0100 |
haftmann |
generalized type signature of foldSet, fold
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 04:11:06 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sat, 18 Nov 2006 00:20:16 +0100 |
haftmann |
clarified module dependencies
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 19:48:34 +0100 |
haftmann |
renamed Lattice_Locales to Lattices
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 14:03:04 +0100 |
haftmann |
made locale partial_order compatible with axclass order
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 09:33:47 +0100 |
krauss |
* Added annihilation axioms ("x * 0 = 0") to axclass semiring_0.
|
file |
diff |
annotate
|
| Tue, 04 Jul 2006 14:47:01 +0200 |
ballarin |
Method intro_locales replaced by intro_locales and unfold_locales.
|
file |
diff |
annotate
|
| Tue, 20 Jun 2006 15:53:44 +0200 |
ballarin |
Restructured locales with predicates: import is now an interpretation.
|
file |
diff |
annotate
|
| Tue, 13 Jun 2006 15:07:58 +0200 |
paulson |
new results
|
file |
diff |
annotate
|
| Mon, 12 Jun 2006 22:14:38 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 06 Jun 2006 17:07:27 +0200 |
paulson |
new lemmas concerning finite cardinalities
|
file |
diff |
annotate
|
| 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
|