| 2009-06-04 |
haftmann |
2009-06-04 |
lemma about List.foldl and Finite_Set.fold
|
file | diff | annotate |
| 2009-06-02 |
hoelzl |
2009-06-02 |
Added theorems about distinct & concat, map & replicate and concat & replicate
|
file | diff | annotate |
| 2009-05-27 |
nipkow |
2009-05-27 |
more lemmas
|
file | diff | annotate |
| 2009-05-26 |
huffman |
2009-05-26 |
listsum lemmas
|
file | diff | annotate |
| 2009-05-19 |
nipkow |
2009-05-19 |
new lemma
|
file | diff | annotate |
| 2009-05-15 |
nipkow |
2009-05-15 |
new lemma
|
file | diff | annotate |
| 2009-05-14 |
haftmann |
2009-05-14 |
preprocessing must consider eq
|
file | diff | annotate |
| 2009-05-09 |
nipkow |
2009-05-09 |
lemmas by Andreas Lochbihler
|
file | diff | annotate |
| 2009-05-08 |
nipkow |
2009-05-08 |
more lemmas
|
file | diff | annotate |
| 2009-05-06 |
haftmann |
2009-05-06 |
proper structures for list and string code generation stuff
|
file | diff | annotate |
| 2009-05-06 |
haftmann |
2009-05-06 |
refined HOL string theories and corresponding ML fragments
|
file | diff | annotate |
| 2009-04-29 |
nipkow |
2009-04-29 |
added listsum lemmas
|
file | diff | annotate |
| 2009-04-24 |
haftmann |
2009-04-24 |
funpow and relpow with shared "^^" syntax
|
file | diff | annotate |
| 2009-04-20 |
haftmann |
2009-04-20 |
power operation on functions with syntax o^; power operation on relations with syntax ^^
|
file | diff | annotate |
| 2009-04-17 |
haftmann |
2009-04-17 |
separated funpow, relpow from power on monoids
|
file | diff | annotate |
| 2009-03-04 |
blanchet |
2009-03-04 |
Merge.
|
file | diff | annotate |
| 2009-03-04 |
blanchet |
2009-03-04 |
Merge.
|
file | diff | annotate |
| 2009-03-02 |
nipkow |
2009-03-02 |
name changes
|
file | diff | annotate |
| 2009-02-26 |
huffman |
2009-02-26 |
revert some Suc 0 lemmas back to their original forms; added some simp rules for (1::nat)
|
file | diff | annotate |
| 2009-02-23 |
huffman |
2009-02-23 |
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
|
file | diff | annotate |
| 2009-02-20 |
haftmann |
2009-02-20 |
defensive implementation of pretty serialisation of lists and characters
|
file | diff | annotate |
| 2009-02-16 |
blanchet |
2009-02-16 |
Added nitpick attribute, and fixed typo.
|
file | diff | annotate |
| 2009-02-10 |
huffman |
2009-02-10 |
const_name antiquotations
|
file | diff | annotate |
| 2009-02-07 |
haftmann |
2009-02-07 |
code theorems for nth, list_update
|
file | diff | annotate |
| 2009-02-07 |
haftmann |
2009-02-07 |
code theorems for nth, list_update
|
file | diff | annotate |
| 2009-02-06 |
haftmann |
2009-02-06 |
authentic syntax for List.nth
|
file | diff | annotate |
| 2009-02-03 |
haftmann |
2009-02-03 |
dropped global Nil/Append interpretation
|
file | diff | annotate |
| 2009-01-26 |
haftmann |
2009-01-26 |
sorted_take, sorted_drop
|
file | diff | annotate |
| 2009-01-16 |
haftmann |
2009-01-16 |
migrated class package to new locale implementation
|
file | diff | annotate |
| 2008-12-31 |
wenzelm |
2008-12-31 |
eliminated OldTerm.add_term_free_names;
|
file | diff | annotate |
| 2008-12-31 |
wenzelm |
2008-12-31 |
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
|
file | diff | annotate |
| 2008-12-11 |
ballarin |
2008-12-11 |
Conversion of HOL-Main and ZF to new locales.
|
file | diff | annotate |
| 2008-12-04 |
haftmann |
2008-12-04 |
cleaned up binding module and related code
|
file | diff | annotate |
| 2008-11-17 |
haftmann |
2008-11-17 |
tuned unfold_locales invocation
|
file | diff | annotate |
| 2008-11-14 |
haftmann |
2008-11-14 |
added length_unique operation for code generation
|
file | diff | annotate |
| 2008-10-29 |
haftmann |
2008-10-29 |
explicit check for pattern discipline before code translation
|
file | diff | annotate |
| 2008-10-22 |
haftmann |
2008-10-22 |
code identifier namings are no longer imperative
|
file | diff | annotate |
| 2008-10-20 |
nipkow |
2008-10-20 |
added lemmas
|
file | diff | annotate |
| 2008-10-10 |
haftmann |
2008-10-10 |
`code func` now just `code`
|
file | diff | annotate |
| 2008-10-09 |
haftmann |
2008-10-09 |
established canonical argument order in SML code generators
|
file | diff | annotate |
| 2008-10-07 |
haftmann |
2008-10-07 |
dropped superfluous if
|
file | diff | annotate |
| 2008-09-26 |
haftmann |
2008-09-26 |
removed obsolete name convention "func"
|
file | diff | annotate |
| 2008-09-25 |
haftmann |
2008-09-25 |
discontinued special treatment of op = vs. eq_class.eq
|
file | diff | annotate |
| 2008-09-17 |
wenzelm |
2008-09-17 |
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
|
file | diff | annotate |
| 2008-09-16 |
haftmann |
2008-09-16 |
a sophisticated char/nibble conversion combinator
|
file | diff | annotate |
| 2008-09-16 |
haftmann |
2008-09-16 |
explicit size of characters
|
file | diff | annotate |
| 2008-09-02 |
haftmann |
2008-09-02 |
distributed literal code generation out of central infrastructure
|
file | diff | annotate |
| 2008-09-01 |
nipkow |
2008-09-01 |
It appears that the code generator (Stefan's) needs some laws that appear superfluous: {..n} = set ...
|
file | diff | annotate |
| 2008-09-01 |
nipkow |
2008-09-01 |
cleaned up code generation for {.._} and {..<_}
moved lemmas into SetInterval where they belong
|
file | diff | annotate |
| 2008-09-01 |
haftmann |
2008-09-01 |
restructured code generation of literals
|
file | diff | annotate |
| 2008-08-28 |
haftmann |
2008-08-28 |
restructured and split code serializer module
|
file | diff | annotate |
| 2008-08-01 |
nipkow |
2008-08-01 |
made setsum executable on int.
|
file | diff | annotate |
| 2008-07-29 |
nipkow |
2008-07-29 |
added removeAll
|
file | diff | annotate |
| 2008-06-28 |
wenzelm |
2008-06-28 |
@{lemma}: 'by' keyword;
|
file | diff | annotate |
| 2008-06-26 |
haftmann |
2008-06-26 |
established Plain theory and image
|
file | diff | annotate |
| 2008-06-10 |
haftmann |
2008-06-10 |
removed some dubious code lemmas
|
file | diff | annotate |
| 2008-05-23 |
berghofe |
2008-05-23 |
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
set print_mode and margin appropriately.
|
file | diff | annotate |
| 2008-05-12 |
krauss |
2008-05-12 |
Measure functions can now be declared via special rules, allowing for a
prolog-style generation of measure functions for a specific type.
|
file | diff | annotate |
| 2008-05-07 |
berghofe |
2008-05-07 |
- Explicitely applied predicate1I in a few proofs, because it is no longer
part of the claset
- Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the
to_set attribute, because it is no longer applied automatically
|
file | diff | annotate |
| 2008-05-02 |
nipkow |
2008-05-02 |
Added documentation
|
file | diff | annotate |