| 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
|
| Thu, 16 Aug 2012 14:07:32 +0200 |
haftmann |
prefer eta-expanded code equations for fold, to accomodate tail recursion optimisation in Scala
|
file |
diff |
annotate
|
| Tue, 31 Jul 2012 13:55:39 +0200 |
kuncar |
more set operations expressed by Finite_Set.fold
|
file |
diff |
annotate
|
| Mon, 30 Apr 2012 12:14:53 +0200 |
bulwahn |
making sorted_list_of_set executable
|
file |
diff |
annotate
|
| Sat, 21 Apr 2012 06:49:04 +0200 |
huffman |
strengthen rule list_all2_induct
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 11:01:15 +0200 |
bulwahn |
merged
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 17:26:30 +0900 |
griff |
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
|
file |
diff |
annotate
|
| Fri, 06 Apr 2012 19:23:51 +0200 |
haftmann |
abandoned almost redundant *_foldr lemmas
|
file |
diff |
annotate
|
| Fri, 06 Apr 2012 19:18:00 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 06 Apr 2012 18:17:16 +0200 |
haftmann |
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
|
file |
diff |
annotate
|
| Mon, 26 Mar 2012 21:00:23 +0200 |
nipkow |
reverted to canonical name
|
file |
diff |
annotate
|
| Mon, 26 Mar 2012 18:54:41 +0200 |
nipkow |
Functions and lemmas by Christian Sternagel
|
file |
diff |
annotate
|
| Sun, 25 Mar 2012 20:15:39 +0200 |
huffman |
merged fork with new numeral representation (see NEWS)
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 13:31:26 +0100 |
wenzelm |
tuned proofs -- eliminated pointless chaining of facts after 'interpret';
|
file |
diff |
annotate
|
| Mon, 12 Mar 2012 21:41:11 +0100 |
noschinl |
tuned proofs
|
file |
diff |
annotate
|
| Mon, 27 Feb 2012 09:01:49 +0100 |
nipkow |
converting "set [...]" to "{...}" in evaluation results
|
file |
diff |
annotate
|
| Sat, 25 Feb 2012 09:07:37 +0100 |
bulwahn |
one general list_all2_update_cong instead of two special ones
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 22:46:44 +0100 |
haftmann |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
|
file |
diff |
annotate
|
| Fri, 24 Feb 2012 09:40:02 +0100 |
haftmann |
given up disfruitful branch
|
file |
diff |
annotate
|
| Thu, 23 Feb 2012 21:25:59 +0100 |
haftmann |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
|
file |
diff |
annotate
|
| Thu, 16 Feb 2012 09:18:23 +0100 |
bulwahn |
removing unnecessary premises in theorems of List theory
|
file |
diff |
annotate
|
| Fri, 10 Feb 2012 09:47:59 +0100 |
Cezary Kaliszyk |
more specification of the quotient package in IsarRef
|
file |
diff |
annotate
|
| Wed, 08 Feb 2012 01:49:33 +0100 |
blanchet |
use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules")
|
file |
diff |
annotate
|
| Wed, 08 Feb 2012 00:55:06 +0100 |
blanchet |
removed fact that confuses SPASS -- better rely on "rev_rev_ident", which is stronger and more ATP friendly
|
file |
diff |
annotate
|
| Sun, 05 Feb 2012 10:43:52 +0100 |
bulwahn |
adding code equation for Relation.image; adding map_project as correspondence to map_filter on lists
|
file |
diff |
annotate
|
| Sun, 05 Feb 2012 08:24:39 +0100 |
bulwahn |
another try to improve code generation of set equality (cf. da32cf32c0c7)
|
file |
diff |
annotate
|
| Thu, 02 Feb 2012 10:12:30 +0100 |
bulwahn |
adding a minimally refined equality on sets for code generation
|
file |
diff |
annotate
|
| Tue, 31 Jan 2012 15:39:45 +0100 |
bulwahn |
adding code equation for setsum
|
file |
diff |
annotate
|
| Mon, 23 Jan 2012 17:29:19 +0100 |
huffman |
generalize type of List.listrel
|
file |
diff |
annotate
|
| Mon, 23 Jan 2012 14:07:36 +0100 |
bulwahn |
adding code generation for some list relations
|
file |
diff |
annotate
|
| Tue, 10 Jan 2012 18:12:03 +0100 |
berghofe |
pred_subset/equals_eq are now standard pred_set_conv rules
|
file |
diff |
annotate
|
| Sat, 07 Jan 2012 20:44:23 +0100 |
haftmann |
massaging of code setup for sets
|
file |
diff |
annotate
|
| Sat, 07 Jan 2012 11:45:53 +0100 |
haftmann |
corrected slip
|
file |
diff |
annotate
|
| Sat, 07 Jan 2012 09:32:01 +0100 |
haftmann |
restore convenient code_abbrev declarations (particulary important if List.set is not the formal constructor for sets)
|
file |
diff |
annotate
|
| Fri, 06 Jan 2012 22:16:01 +0100 |
haftmann |
moved lemmas about List.set and set operations to List theory
|
file |
diff |
annotate
|
| Fri, 06 Jan 2012 20:39:50 +0100 |
haftmann |
farewell to theory More_List
|
file |
diff |
annotate
|
| Fri, 06 Jan 2012 17:44:42 +0100 |
wenzelm |
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup;
|
file |
diff |
annotate
|
| Fri, 06 Jan 2012 10:19:49 +0100 |
haftmann |
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
|
file |
diff |
annotate
|
| Thu, 05 Jan 2012 18:18:39 +0100 |
wenzelm |
improved case syntax: more careful treatment of position constraints, which enables PIDE markup;
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 13:42:21 +0100 |
haftmann |
qualified Finite_Set.fold
|
file |
diff |
annotate
|
| Thu, 29 Dec 2011 10:47:55 +0100 |
haftmann |
attribute code_abbrev superseedes code_unfold_post; tuned text
|
file |
diff |
annotate
|
| Tue, 27 Dec 2011 09:15:26 +0100 |
haftmann |
dropped fact whose names clash with corresponding facts on canonical fold
|
file |
diff |
annotate
|
| Sat, 24 Dec 2011 15:53:10 +0100 |
haftmann |
dropped obsolete lemma member_set
|
file |
diff |
annotate
|
| Mon, 19 Dec 2011 14:41:08 +0100 |
noschinl |
add lemmas
|
file |
diff |
annotate
|
| Thu, 15 Dec 2011 18:08:40 +0100 |
wenzelm |
clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2011 22:44:16 +0100 |
noschinl |
added lemmas
|
file |
diff |
annotate
|