| 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
|