| Thu, 07 Jul 2016 17:34:39 +0200 |
fleury |
more instantiations for multiset
|
file |
diff |
annotate
|
| Thu, 07 Jul 2016 09:24:03 +0200 |
blanchet |
moved lemmas and locales around (with minor incompatibilities)
|
file |
diff |
annotate
|
| Tue, 05 Jul 2016 13:05:04 +0200 |
fleury |
instantiate multiset with multiset ordering
|
file |
diff |
annotate
|
| Wed, 25 May 2016 11:50:58 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2016 10:22:46 +0100 |
haftmann |
more theorems on orderings
|
file |
diff |
annotate
|
| Fri, 26 Feb 2016 22:44:11 +0100 |
haftmann |
more succint formulation of membership for multisets, similar to lists;
|
file |
diff |
annotate
|
| Fri, 19 Jun 2015 15:55:22 +0200 |
nipkow |
renamed multiset_of -> mset
|
file |
diff |
annotate
|
| Wed, 10 Jun 2015 13:24:16 +0200 |
Mathias Fleury |
Renaming multiset operators < ~> <#,...
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
file |
diff |
annotate
|
| Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 22:49:02 +0100 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 15:18:52 +0100 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Wed, 08 Sep 2010 19:21:46 +0200 |
haftmann |
modernized primrec
|
file |
diff |
annotate
|
| Mon, 22 Feb 2010 09:15:12 +0100 |
haftmann |
tuned proofs
|
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, 03 Aug 2007 20:19:41 +0200 |
wenzelm |
misc cleanup of ML bindings (for multihreading);
|
file |
diff |
annotate
|
| Wed, 26 Jul 2006 19:23:04 +0200 |
webertj |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
file |
diff |
annotate
|
| Tue, 03 Jan 2006 15:43:54 +0100 |
paulson |
added explicit paths to required theories
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 16:12:49 +0200 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
| Thu, 22 Jul 2004 17:37:31 +0200 |
nipkow |
Modified \<Sum> syntax a little.
|
file |
diff |
annotate
|
| Thu, 15 Jul 2004 13:11:34 +0200 |
nipkow |
Moved to new m<..<n syntax for set intervals.
|
file |
diff |
annotate
|
| Tue, 11 May 2004 20:11:08 +0200 |
obua |
changes made due to new Ring_and_Field theory
|
file |
diff |
annotate
|
| Mon, 26 Jan 2004 10:34:02 +0100 |
schirmer |
* Support for raw latex output in control symbols: \<^raw...>
|
file |
diff |
annotate
|
| Wed, 16 Jul 2003 12:09:41 +0200 |
paulson |
tidying
|
file |
diff |
annotate
|
| Fri, 31 Jan 2003 20:12:44 +0100 |
paulson |
conversion to new-style theories and tidying
|
file |
diff |
annotate
|
| Fri, 24 Jan 2003 18:13:59 +0100 |
paulson |
More conversion of UNITY to Isar new-style theories
|
file |
diff |
annotate
|
| Mon, 05 Mar 2001 15:32:54 +0100 |
paulson |
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
|
file |
diff |
annotate
|