| Thu, 23 May 2013 14:22:49 +0200 |
noschinl |
more lemmas for sorted_list_of_set
|
file |
diff |
annotate
|
| Mon, 06 May 2013 02:48:18 +0200 |
nipkow |
tail recursive version of map, for code generation, optionally
|
file |
diff |
annotate
|
| Tue, 23 Apr 2013 11:14:51 +0200 |
haftmann |
tuned: unnamed contexts, interpretation and sublocale in locale target;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Fri, 05 Apr 2013 22:08:42 +0200 |
traytel |
allow redundant cases in the list comprehension translation
|
file |
diff |
annotate
|
| Tue, 22 Jan 2013 14:33:45 +0100 |
traytel |
separate data used for case translation from the datatype package
|
file |
diff |
annotate
|
| Tue, 22 Jan 2013 13:32:41 +0100 |
berghofe |
case translations performed in a separate check phase (with adjustments by traytel)
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 10:55:05 +0100 |
haftmann |
centralized various multiset operations in theory multiset;
|
file |
diff |
annotate
|
| Tue, 26 Mar 2013 20:49:57 +0100 |
haftmann |
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
|
file |
diff |
annotate
|
| Sat, 23 Mar 2013 20:50:39 +0100 |
haftmann |
fundamental revision of big operators on sets
|
file |
diff |
annotate
|
| Thu, 28 Feb 2013 17:14:55 +0100 |
wenzelm |
provide common HOLogic.conj_conv and HOLogic.eq_conv;
|
file |
diff |
annotate
|
| Thu, 28 Feb 2013 16:54:52 +0100 |
wenzelm |
just one HOLogic.Trueprop_conv, with regular exception CTERM;
|
file |
diff |
annotate
|
| Mon, 25 Feb 2013 12:17:50 +0100 |
wenzelm |
prefer stateless 'ML_val' for tests;
|
file |
diff |
annotate
|
| Sun, 17 Feb 2013 21:29:30 +0100 |
haftmann |
Sieve of Eratosthenes
|
file |
diff |
annotate
|
| Sun, 17 Feb 2013 11:34:40 +0100 |
haftmann |
simplified construction of upto_aux
|
file |
diff |
annotate
|
| Sat, 16 Feb 2013 15:27:10 +0100 |
nipkow |
tail recursive code for function "upto"
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 11:47:33 +0100 |
haftmann |
systematic conversions between nat and nibble/char;
|
file |
diff |
annotate
|
| Thu, 14 Feb 2013 12:24:42 +0100 |
haftmann |
abandoned theory Plain
|
file |
diff |
annotate
|
| Wed, 13 Feb 2013 13:38:52 +0100 |
haftmann |
combinator List.those;
|
file |
diff |
annotate
|
| Fri, 14 Dec 2012 19:51:20 +0100 |
nipkow |
unified layout of defs
|
file |
diff |
annotate
|
| Fri, 07 Dec 2012 16:25:33 +0100 |
wenzelm |
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time) -- relevant for any application using it, e.g. small paper sessions;
|
file |
diff |
annotate
|
| Tue, 20 Nov 2012 18:59:35 +0100 |
hoelzl |
add Countable_Set theory
|
file |
diff |
annotate
|
| Thu, 08 Nov 2012 11:59:48 +0100 |
bulwahn |
adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs
|
file |
diff |
annotate
|
| Sun, 21 Oct 2012 17:04:13 +0200 |
webertj |
merged
|
file |
diff |
annotate
|
| Fri, 19 Oct 2012 15:12:52 +0200 |
webertj |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file |
diff |
annotate
|
| Sat, 20 Oct 2012 09:12:16 +0200 |
haftmann |
moved quite generic material from theory Enum to more appropriate places
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 15:16:44 +0200 |
Andreas Lochbihler |
tail-recursive implementation for length
|
file |
diff |
annotate
|
| Tue, 09 Oct 2012 16:57:58 +0200 |
kuncar |
rename Set.project to Set.filter - more appropriate name
|
file |
diff |
annotate
|
| Mon, 08 Oct 2012 12:03:49 +0200 |
haftmann |
consolidated names of theorems on composition;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|