| 2010-10-27 |
haftmann |
2010-10-27 |
sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
|
file | diff | annotate |
| 2010-10-26 |
haftmann |
2010-10-26 |
include ATP in theory List -- avoid theory edge by-passing the prominent list theory
|
file | diff | annotate |
| 2010-10-25 |
haftmann |
2010-10-25 |
dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
|
file | diff | annotate |
| 2010-10-24 |
nipkow |
2010-10-24 |
nat_number -> eval_nat_numeral
|
file | diff | annotate |
| 2010-10-06 |
blanchet |
2010-10-06 |
merged
|
file | diff | annotate |
| 2010-10-04 |
blanchet |
2010-10-04 |
move Metis into Plain
|
file | diff | annotate |
| 2010-10-04 |
haftmann |
2010-10-04 |
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
|
file | diff | annotate |
| 2010-09-28 |
haftmann |
2010-09-28 |
localized listsum
|
file | diff | annotate |
| 2010-09-27 |
haftmann |
2010-09-27 |
lemma remdups_map_remdups
|
file | diff | annotate |
| 2010-09-22 |
nipkow |
2010-09-22 |
more lists lemmas
|
file | diff | annotate |
| 2010-09-21 |
nipkow |
2010-09-21 |
new lemma
|
file | diff | annotate |
| 2010-09-17 |
haftmann |
2010-09-17 |
generalized lemma insort_remove1 to insort_key_remove1
|
file | diff | annotate |
| 2010-09-13 |
nipkow |
2010-09-13 |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file | diff | annotate |
| 2010-09-10 |
haftmann |
2010-09-10 |
Haskell == is infix, not infixl
|
file | diff | annotate |
| 2010-09-07 |
nipkow |
2010-09-07 |
expand_fun_eq -> ext_iff
expand_set_eq -> set_ext_iff
Naming in line now with multisets
|
file | diff | annotate |
| 2010-09-02 |
hoelzl |
2010-09-02 |
Add filter_remove1
|
file | diff | annotate |
| 2010-08-27 |
haftmann |
2010-08-27 |
renamed class/constant eq to equal; tuned some instantiations
|
file | diff | annotate |
| 2010-08-25 |
wenzelm |
2010-08-25 |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
file | diff | annotate |
| 2010-07-19 |
haftmann |
2010-07-19 |
Scala: subtle difference in printing strings vs. complex mixfix syntax
|
file | diff | annotate |
| 2010-07-12 |
haftmann |
2010-07-12 |
dropped superfluous [code del]s
|
file | diff | annotate |
| 2010-06-28 |
haftmann |
2010-06-28 |
put section on distinctness before listsum; refined code generation operations; dropped ancient infix mem
|
file | diff | annotate |
| 2010-06-18 |
haftmann |
2010-06-18 |
merged
|
file | diff | annotate |
| 2010-06-18 |
haftmann |
2010-06-18 |
made List.thy a join point in the theory graph
|
file | diff | annotate |
| 2010-06-18 |
nipkow |
2010-06-18 |
tuned set_replicate lemmas
|
file | diff | annotate |
| 2010-06-18 |
nipkow |
2010-06-18 |
merged
|
file | diff | annotate |
| 2010-06-18 |
nipkow |
2010-06-18 |
added lemmas
|
file | diff | annotate |
| 2010-06-17 |
haftmann |
2010-06-17 |
rev is reverse in Haskell
|
file | diff | annotate |
| 2010-06-14 |
haftmann |
2010-06-14 |
use various predefined Haskell operations when generating code
|
file | diff | annotate |
| 2010-06-12 |
haftmann |
2010-06-12 |
declare lexn.simps [code del]
|
file | diff | annotate |
| 2010-06-02 |
haftmann |
2010-06-02 |
induction over non-empty lists
|
file | diff | annotate |
| 2010-05-26 |
haftmann |
2010-05-26 |
more convenient order of code equations
|
file | diff | annotate |
| 2010-05-24 |
haftmann |
2010-05-24 |
more lemmas
|
file | diff | annotate |
| 2010-05-20 |
haftmann |
2010-05-20 |
turned old-style mem into an input abbreviation
|
file | diff | annotate |
| 2010-05-14 |
nipkow |
2010-05-14 |
added listsum lemmas
|
file | diff | annotate |
| 2010-05-13 |
nipkow |
2010-05-13 |
Multiset: renamed, added and tuned lemmas;
Permutation: replaced local "remove" by List.remove1
|
file | diff | annotate |
| 2010-05-12 |
haftmann |
2010-05-12 |
added lemmas concerning last, butlast, insort
|
file | diff | annotate |
| 2010-04-20 |
hoelzl |
2010-04-20 |
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
|
file | diff | annotate |
| 2010-04-22 |
haftmann |
2010-04-22 |
lemmas concerning remdups
|
file | diff | annotate |
| 2010-04-19 |
haftmann |
2010-04-19 |
merged
|
file | diff | annotate |
| 2010-04-19 |
haftmann |
2010-04-19 |
more convenient equations for zip
|
file | diff | annotate |
| 2010-04-16 |
wenzelm |
2010-04-16 |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file | diff | annotate |
| 2010-04-15 |
Cezary Kaliszyk |
2010-04-15 |
Respectfullness and preservation of list_rel
|
file | diff | annotate |
| 2010-03-18 |
blanchet |
2010-03-18 |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file | diff | annotate |
| 2010-03-17 |
blanchet |
2010-03-17 |
renamed "ATP_Linkup" theory to "Sledgehammer"
|
file | diff | annotate |
| 2010-03-06 |
haftmann |
2010-03-06 |
added insort_insert
|
file | diff | annotate |
| 2010-03-05 |
haftmann |
2010-03-05 |
moved lemma map_sorted_distinct_set_unique
|
file | diff | annotate |
| 2010-03-02 |
paulson |
2010-03-02 |
Slightly generalised a theorem
|
file | diff | annotate |
| 2010-02-22 |
haftmann |
2010-02-22 |
merged
|
file | diff | annotate |
| 2010-02-20 |
haftmann |
2010-02-20 |
lemma distinct_insert
|
file | diff | annotate |
| 2010-02-22 |
haftmann |
2010-02-22 |
merged
|
file | diff | annotate |
| 2010-02-19 |
haftmann |
2010-02-19 |
moved remaning class operations from Algebras.thy to Groups.thy
|
file | diff | annotate |
| 2010-02-21 |
wenzelm |
2010-02-21 |
adapted to authentic syntax;
|
file | diff | annotate |
| 2010-02-20 |
nipkow |
2010-02-20 |
added lemma
|
file | diff | annotate |
| 2010-02-18 |
huffman |
2010-02-18 |
merged
|
file | diff | annotate |
| 2010-02-18 |
huffman |
2010-02-18 |
get rid of many duplicate simp rule warnings
|
file | diff | annotate |
| 2010-02-18 |
nipkow |
2010-02-18 |
added lemma
|
file | diff | annotate |
| 2010-02-17 |
haftmann |
2010-02-17 |
more lemmas about sort(_key)
|
file | diff | annotate |
| 2010-02-11 |
wenzelm |
2010-02-11 |
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
|
file | diff | annotate |
| 2010-02-05 |
haftmann |
2010-02-05 |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
file | diff | annotate |
| 2010-01-31 |
haftmann |
2010-01-31 |
canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply
|
file | diff | annotate |