Tue, 23 Feb 2010 08:08:23 +0100 |
haftmann |
mind the "s"
|
file |
diff |
annotate
|
Mon, 22 Feb 2010 09:15:11 +0100 |
haftmann |
ascii syntax for multiset order
|
file |
diff |
annotate
|
Fri, 19 Feb 2010 16:52:00 +0100 |
haftmann |
switched notations for pointwise and multiset order
|
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
|
Fri, 22 Jan 2010 13:38:28 +0100 |
haftmann |
cleanup of Multiset.thy: less duplication, tuned and simplified a couple of proofs, less historical organization of sections, conversion from associations lists to multisets, rudimentary code generation
|
file |
diff |
annotate
|
Sun, 25 Oct 2009 00:00:53 +0200 |
wenzelm |
adapted Function_Lib (cf. b8cdd3d73022);
|
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
|
Fri, 28 Aug 2009 19:35:49 +0200 |
nipkow |
tuned proofs
|
file |
diff |
annotate
|
Thu, 26 Mar 2009 20:08:55 +0100 |
wenzelm |
interpretation/interpret: prefixes are mandatory by default;
|
file |
diff |
annotate
|
Mon, 23 Mar 2009 08:14:24 +0100 |
haftmann |
Main is (Complex_Main) base entry point in library theories
|
file |
diff |
annotate
|
Thu, 19 Mar 2009 22:05:00 +0100 |
wenzelm |
proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
|
file |
diff |
annotate
|
Wed, 11 Mar 2009 08:45:46 +0100 |
haftmann |
explicitly delete some code equations
|
file |
diff |
annotate
|
Fri, 13 Feb 2009 23:55:04 +0100 |
nipkow |
finiteness lemmas
|
file |
diff |
annotate
|
Fri, 16 Jan 2009 14:58:11 +0100 |
haftmann |
migrated class package to new locale implementation
|
file |
diff |
annotate
|
Tue, 30 Dec 2008 11:10:01 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
Sun, 14 Dec 2008 18:45:51 +0100 |
ballarin |
Ported HOL and HOL-Library to new locales.
|
file |
diff |
annotate
|
Tue, 16 Dec 2008 08:46:07 +0100 |
krauss |
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
|
file |
diff |
annotate
|
Mon, 17 Nov 2008 17:00:55 +0100 |
haftmann |
tuned unfold_locales invocation
|
file |
diff |
annotate
|
Wed, 29 Oct 2008 11:33:40 +0100 |
haftmann |
explicit check for pattern discipline before code translation
|
file |
diff |
annotate
|
Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
Fri, 25 Jul 2008 12:03:34 +0200 |
haftmann |
added class preorder
|
file |
diff |
annotate
|
Tue, 15 Jul 2008 16:50:09 +0200 |
ballarin |
Removed uses of context element includes.
|
file |
diff |
annotate
|
Mon, 07 Jul 2008 08:47:17 +0200 |
haftmann |
absolute imports of HOL/*.thy theories
|
file |
diff |
annotate
|
Thu, 26 Jun 2008 10:07:01 +0200 |
haftmann |
established Plain theory and image
|
file |
diff |
annotate
|
Tue, 10 Jun 2008 15:30:56 +0200 |
haftmann |
removed some dubious code lemmas
|
file |
diff |
annotate
|
Wed, 07 May 2008 10:59:33 +0200 |
berghofe |
Instantiated rule expand_fun_eq in proof of set_of_eq_empty_iff, to avoid that
|
file |
diff |
annotate
|
Mon, 07 Apr 2008 15:37:34 +0200 |
haftmann |
instantiation replacing primitive instance plus overloaded defs; more conservative type arities
|
file |
diff |
annotate
|
Thu, 28 Feb 2008 14:04:29 +0100 |
nipkow |
tuned
|
file |
diff |
annotate
|
Thu, 28 Feb 2008 12:56:31 +0100 |
wenzelm |
tuned syntax declaration;
|
file |
diff |
annotate
|
Tue, 26 Feb 2008 16:10:54 +0100 |
wenzelm |
tuned document;
|
file |
diff |
annotate
|
Tue, 26 Feb 2008 11:18:43 +0100 |
bulwahn |
Added useful general lemmas from the work with the HeapMonad
|
file |
diff |
annotate
|
Fri, 01 Feb 2008 18:01:06 +0100 |
nipkow |
modified MCollect syntax
|
file |
diff |
annotate
|
Wed, 30 Jan 2008 17:34:21 +0100 |
nipkow |
added multiset comprehension
|
file |
diff |
annotate
|
Wed, 02 Jan 2008 04:10:47 +0100 |
kleing |
renamed foldM to fold_mset on general request
|
file |
diff |
annotate
|
Thu, 13 Dec 2007 22:35:45 +0100 |
kleing |
removed syntax in locale left_commutative
|
file |
diff |
annotate
|
Thu, 13 Dec 2007 07:09:23 +0100 |
haftmann |
changed order in class parameters
|
file |
diff |
annotate
|
Thu, 13 Dec 2007 06:51:22 +0100 |
kleing |
a fold operation for multisets + more lemmas
|
file |
diff |
annotate
|
Mon, 10 Dec 2007 11:24:12 +0100 |
haftmann |
switched import from Main to List
|
file |
diff |
annotate
|
Fri, 07 Dec 2007 15:07:59 +0100 |
haftmann |
instantiation target rather than legacy instance
|
file |
diff |
annotate
|
Fri, 30 Nov 2007 11:51:22 +0100 |
nipkow |
added {#.,.,...#}
|
file |
diff |
annotate
|
Fri, 26 Oct 2007 21:22:19 +0200 |
haftmann |
changed order of class parameters
|
file |
diff |
annotate
|
Tue, 23 Oct 2007 23:27:23 +0200 |
nipkow |
went back to >0
|
file |
diff |
annotate
|
Sun, 21 Oct 2007 22:33:35 +0200 |
nipkow |
More changes from >0 to ~=0::nat
|
file |
diff |
annotate
|
Sun, 21 Oct 2007 14:53:44 +0200 |
nipkow |
Eliminated most of the neq0_conv occurrences. As a result, many
|
file |
diff |
annotate
|
Sun, 29 Jul 2007 14:29:49 +0200 |
wenzelm |
simplified ResAtpset via NamedThmsFun;
|
file |
diff |
annotate
|
Wed, 11 Jul 2007 11:24:36 +0200 |
berghofe |
Restored set notation.
|
file |
diff |
annotate
|
Fri, 06 Jul 2007 23:26:13 +0200 |
nipkow |
more interpretations
|
file |
diff |
annotate
|
Wed, 13 Jun 2007 18:30:11 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
Wed, 06 Jun 2007 19:12:59 +0200 |
nipkow |
changed filter syntax from : to <-
|
file |
diff |
annotate
|
Wed, 14 Feb 2007 10:06:12 +0100 |
haftmann |
added class "preorder"
|
file |
diff |
annotate
|
Wed, 07 Feb 2007 17:41:11 +0100 |
berghofe |
Converted to predicate notation.
|
file |
diff |
annotate
|
Sat, 18 Nov 2006 00:20:26 +0100 |
haftmann |
using class instance
|
file |
diff |
annotate
|
Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
Tue, 07 Nov 2006 14:02:10 +0100 |
haftmann |
adjusted two lemma names due to name change in interpretation
|
file |
diff |
annotate
|
Thu, 28 Sep 2006 23:42:43 +0200 |
wenzelm |
fixed translations: CONST;
|
file |
diff |
annotate
|
Mon, 11 Sep 2006 21:35:19 +0200 |
wenzelm |
induct method: renamed 'fixing' to 'arbitrary';
|
file |
diff |
annotate
|
Fri, 05 May 2006 22:11:19 +0200 |
wenzelm |
get rid of 'concl is';
|
file |
diff |
annotate
|
Fri, 05 May 2006 17:17:21 +0200 |
krauss |
First usable version of the new function definition package (HOL/function_packake/...).
|
file |
diff |
annotate
|
Sat, 08 Apr 2006 22:51:06 +0200 |
wenzelm |
refined 'abbreviation';
|
file |
diff |
annotate
|
Thu, 16 Feb 2006 21:12:00 +0100 |
wenzelm |
new-style definitions/abbreviations;
|
file |
diff |
annotate
|