| Mon, 01 Mar 2010 13:40:23 +0100 |
haftmann |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
file |
diff |
annotate
|
| Thu, 22 Oct 2009 09:27:48 +0200 |
nipkow |
inv_onto -> inv_into
|
file |
diff |
annotate
|
| Sun, 18 Oct 2009 12:07:56 +0200 |
nipkow |
merged
|
file |
diff |
annotate
|
| Sun, 18 Oct 2009 12:07:25 +0200 |
nipkow |
Inv -> inv_onto, inv abbr. inv_onto UNIV.
|
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
|
| Mon, 22 Jun 2009 20:59:12 +0200 |
nipkow |
tuned FuncSet
|
file |
diff |
annotate
|
| Fri, 19 Jun 2009 22:49:12 +0200 |
nipkow |
Made Pi_I [simp]
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 20:08:55 +0100 |
wenzelm |
interpretation/interpret: prefixes are mandatory by default;
|
file |
diff |
annotate
|
| Wed, 17 Dec 2008 17:53:56 +0100 |
ballarin |
More porting to new locales.
|
file |
diff |
annotate
|
| Tue, 16 Dec 2008 21:10:53 +0100 |
ballarin |
More porting to new locales.
|
file |
diff |
annotate
|
| Mon, 17 Nov 2008 17:00:55 +0100 |
haftmann |
tuned unfold_locales invocation
|
file |
diff |
annotate
|
| Thu, 31 Jul 2008 09:49:21 +0200 |
ballarin |
Tuned (for the sake of a meaningless log entry).
|
file |
diff |
annotate
|
| Wed, 30 Jul 2008 19:03:33 +0200 |
ballarin |
New locales for orders and lattices where the equivalence relation is not restricted to equality.
|
file |
diff |
annotate
|
| Tue, 29 Jul 2008 16:17:13 +0200 |
ballarin |
Unit_inv_l, Unit_inv_r made [simp].
|
file |
diff |
annotate
|
| Tue, 15 Jul 2008 16:50:09 +0200 |
ballarin |
Removed uses of context element includes.
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:56:58 +0200 |
berghofe |
Replaced forward proofs of existential statements by backward proofs
|
file |
diff |
annotate
|
| Wed, 05 Mar 2008 21:24:03 +0100 |
wenzelm |
explicit referencing of background facts;
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 00:01:41 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Fri, 12 Jan 2007 15:37:21 +0100 |
ballarin |
Reverted to structure representation with records.
|
file |
diff |
annotate
|
| Mon, 16 Oct 2006 10:27:54 +0200 |
ballarin |
Order and lattice structures no longer based on records.
|
file |
diff |
annotate
|
| Thu, 03 Aug 2006 14:57:26 +0200 |
ballarin |
Restructured algebra library, added ideals and quotient rings.
|
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, 04 Jul 2006 11:35:49 +0200 |
ballarin |
Minor new lemmas.
|
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, 06 Jun 2006 10:05:57 +0200 |
ballarin |
Improved parameter management of locales.
|
file |
diff |
annotate
|
| Mon, 22 May 2006 22:29:18 +0200 |
wenzelm |
removed unchecked'';
|
file |
diff |
annotate
|
| Sat, 20 May 2006 23:36:51 +0200 |
wenzelm |
pow: unchecked;
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Mon, 18 Apr 2005 09:25:23 +0200 |
ballarin |
Interpretation supports statically scoped attributes; documentation.
|
file |
diff |
annotate
|
| Mon, 11 Apr 2005 12:34:34 +0200 |
ballarin |
First release of interpretation commands.
|
file |
diff |
annotate
|
| Mon, 26 Jul 2004 15:48:50 +0200 |
ballarin |
New prover for transitive and reflexive-transitive closure of relations.
|
file |
diff |
annotate
|
| Thu, 17 Jun 2004 17:18:30 +0200 |
paulson |
removal of magmas and semigroups
|
file |
diff |
annotate
|
| Tue, 01 Jun 2004 11:25:01 +0200 |
paulson |
tidied
|
file |
diff |
annotate
|
| Wed, 26 May 2004 11:43:50 +0200 |
paulson |
more group isomorphisms
|
file |
diff |
annotate
|
| Wed, 19 May 2004 11:30:18 +0200 |
paulson |
more results about isomorphisms
|
file |
diff |
annotate
|
| Fri, 14 May 2004 19:29:22 +0200 |
ballarin |
Change of theory hierarchy: Group is now based in Lattice.
|
file |
diff |
annotate
|
| Thu, 06 May 2004 14:14:18 +0200 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
| Sat, 01 May 2004 22:05:05 +0200 |
wenzelm |
improved syntax;
|
file |
diff |
annotate
|
| Thu, 22 Apr 2004 11:01:34 +0200 |
wenzelm |
improved notation;
|
file |
diff |
annotate
|
| Tue, 13 Apr 2004 09:42:40 +0200 |
ballarin |
Various changes to HOL-Algebra;
|
file |
diff |
annotate
|
| Wed, 10 Dec 2003 14:29:05 +0100 |
ballarin |
New structure "partial_object" as common root for lattices and magmas.
|
file |
diff |
annotate
|
| Thu, 06 Nov 2003 14:18:05 +0100 |
ballarin |
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
|
file |
diff |
annotate
|
| Wed, 07 May 2003 22:07:33 +0200 |
ballarin |
Small changes for release Isabelle 2003.
|
file |
diff |
annotate
|
| Fri, 02 May 2003 20:02:50 +0200 |
ballarin |
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
|
file |
diff |
annotate
|
| Thu, 01 May 2003 11:54:18 +0200 |
paulson |
new proofs about direct products, etc.
|
file |
diff |
annotate
|
| Thu, 01 May 2003 10:29:44 +0200 |
paulson |
moving Bij.thy from GroupTheory to Algebra
|
file |
diff |
annotate
|
| Wed, 30 Apr 2003 18:32:06 +0200 |
ballarin |
HOL-Algebra: New polynomial development added.
|
file |
diff |
annotate
|
| Wed, 30 Apr 2003 10:01:35 +0200 |
ballarin |
Greatly extended CRing. Added Module.
|
file |
diff |
annotate
|
| Mon, 10 Mar 2003 17:25:34 +0100 |
ballarin |
First distributed version of Group and Ring theory.
|
file |
diff |
annotate
|
| Thu, 27 Feb 2003 15:12:29 +0100 |
ballarin |
Change to meta simplifier: congruence rules may now have frees as head of term.
|
file |
diff |
annotate
|
| Fri, 14 Feb 2003 17:35:56 +0100 |
ballarin |
Product operator added --- preliminary.
|
file |
diff |
annotate
|
| Mon, 10 Feb 2003 09:45:22 +0100 |
ballarin |
New development of algebra: Groups.
|
file |
diff |
annotate
|