| 2015-06-01 |
haftmann |
2015-06-01 |
separate class for division operator, with particular syntax added in more specific classes
|
file | diff | annotate |
| 2015-03-23 |
haftmann |
2015-03-23 |
distributivity of partial minus establishes desired properties of dvd in semirings
|
file | diff | annotate |
| 2015-02-06 |
haftmann |
2015-02-06 |
default abstypes and default abstract equations make technical (no_code) annotation superfluous
|
file | diff | annotate |
| 2014-11-02 |
wenzelm |
2014-11-02 |
modernized header uniformly as section;
|
file | diff | annotate |
| 2014-09-18 |
haftmann |
2014-09-18 |
always annotate potentially polymorphic Haskell numerals
|
file | diff | annotate |
| 2014-09-18 |
haftmann |
2014-09-18 |
tuned
|
file | diff | annotate |
| 2014-09-19 |
blanchet |
2014-09-19 |
keep obsolete interpretations in Main, to avoid merge trouble
|
file | diff | annotate |
| 2014-09-18 |
blanchet |
2014-09-18 |
reintroduced an instantiation of 'size' for 'numerals'
|
file | diff | annotate |
| 2014-09-18 |
blanchet |
2014-09-18 |
moved old 'size' generator together with 'old_datatype'
|
file | diff | annotate |
| 2014-09-11 |
blanchet |
2014-09-11 |
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
|
file | diff | annotate |
| 2014-07-04 |
haftmann |
2014-07-04 |
reduced name variants for assoc and commute on plus and mult
|
file | diff | annotate |
| 2014-05-04 |
blanchet |
2014-05-04 |
renamed 'xxx_size' to 'size_xxx' for old datatype package
|
file | diff | annotate |
| 2014-03-06 |
blanchet |
2014-03-06 |
renamed 'fun_rel' to 'rel_fun'
|
file | diff | annotate |
| 2014-02-25 |
kuncar |
2014-02-25 |
unregister lifting setup following the best practice of Lifting
|
file | diff | annotate |
| 2014-02-21 |
blanchet |
2014-02-21 |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
file | diff | annotate |
| 2014-02-12 |
Andreas Lochbihler |
2014-02-12 |
merged
|
file | diff | annotate |
| 2014-02-12 |
Andreas Lochbihler |
2014-02-12 |
make integer_of_char and char_of_integer work with NBE and code_simp
|
file | diff | annotate |
| 2014-02-12 |
blanchet |
2014-02-12 |
adapted theories to 'xxx_case' to 'case_xxx'
* * *
'char_case' -> 'case_char' and same for 'rec'
* * *
compile
* * *
renamed 'xxx_case' to 'case_xxx'
|
file | diff | annotate |
| 2014-02-12 |
blanchet |
2014-02-12 |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
file | diff | annotate |
| 2013-11-19 |
haftmann |
2013-11-19 |
eliminiated neg_numeral in favour of - (numeral _)
|
file | diff | annotate |
| 2013-08-18 |
haftmann |
2013-08-18 |
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
|
file | diff | annotate |
| 2013-06-23 |
haftmann |
2013-06-23 |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
|
file | diff | annotate |
| 2013-03-08 |
kuncar |
2013-03-08 |
patch Isabelle ditribution to conform to changes regarding the parametricity
|
file | diff | annotate |
| 2013-02-15 |
haftmann |
2013-02-15 |
two target language numeral types: integer and natural, as replacement for code_numeral;
former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral;
refined stack of theories implementing int and/or nat by target language numerals;
reduced number of target language numeral types to exactly one
|
file | diff | annotate |
| 2012-10-19 |
webertj |
2012-10-19 |
Renamed {left,right}_distrib to distrib_{right,left}.
|
file | diff | annotate |
| 2012-10-12 |
wenzelm |
2012-10-12 |
discontinued obsolete typedef (open) syntax;
|
file | diff | annotate |
| 2012-07-23 |
haftmann |
2012-07-23 |
restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
|
file | diff | annotate |
| 2012-04-01 |
huffman |
2012-04-01 |
removed Nat_Numeral.thy, moving all theorems elsewhere
|
file | diff | annotate |
| 2012-03-25 |
huffman |
2012-03-25 |
merged fork with new numeral representation (see NEWS)
|
file | diff | annotate |
| 2012-02-24 |
haftmann |
2012-02-24 |
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 |
| 2012-02-24 |
haftmann |
2012-02-24 |
given up disfruitful branch
|
file | diff | annotate |
| 2012-02-23 |
haftmann |
2012-02-23 |
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 |
| 2012-02-20 |
huffman |
2012-02-20 |
use qualified constant names instead of suffixes (from Florian Haftmann)
|
file | diff | annotate |
| 2011-12-29 |
haftmann |
2011-12-29 |
attribute code_abbrev superseedes code_unfold_post
|
file | diff | annotate |
| 2011-11-30 |
wenzelm |
2011-11-30 |
prefer typedef without extra definition and alternative name;
tuned proofs;
|
file | diff | annotate |
| 2011-09-07 |
huffman |
2011-09-07 |
avoid using legacy theorem names
|
file | diff | annotate |
| 2010-10-01 |
haftmann |
2010-10-01 |
use module integer for Eval
|
file | diff | annotate |
| 2010-09-10 |
haftmann |
2010-09-10 |
Haskell == is infix, not infixl
|
file | diff | annotate |
| 2010-08-27 |
haftmann |
2010-08-27 |
renamed class/constant eq to equal; tuned some instantiations
|
file | diff | annotate |
| 2010-07-24 |
haftmann |
2010-07-24 |
another refinement chapter in the neverending numeral story
|
file | diff | annotate |
| 2010-07-23 |
haftmann |
2010-07-23 |
avoid unreliable Haskell Int type
|
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-03-31 |
bulwahn |
2010-03-31 |
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
|
file | diff | annotate |
| 2010-03-10 |
haftmann |
2010-03-10 |
tuned whitespace
|
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-22 |
haftmann |
2010-01-22 |
code literals: distinguish numeral classes by different entries
|
file | diff | annotate |
| 2010-01-15 |
berghofe |
2010-01-15 |
merged
|
file | diff | annotate |
| 2010-01-10 |
berghofe |
2010-01-10 |
Adapted to changes in induct method.
|
file | diff | annotate |
| 2010-01-14 |
haftmann |
2010-01-14 |
allow individual printing of numerals during code serialization
|
file | diff | annotate |
| 2010-01-13 |
haftmann |
2010-01-13 |
some syntax setup for Scala
|
file | diff | annotate |
| 2009-10-29 |
haftmann |
2009-10-29 |
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
|
file | diff | annotate |
| 2009-10-29 |
haftmann |
2009-10-29 |
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
|
file | diff | annotate |
| 2009-10-28 |
haftmann |
2009-10-28 |
moved theory Divides after theory Nat_Numeral; tuned some proof texts
|
file | diff | annotate |
| 2009-07-14 |
haftmann |
2009-07-14 |
prefer code_inline over code_unfold; use code_unfold_post where appropriate
|
file | diff | annotate |
| 2009-07-14 |
haftmann |
2009-07-14 |
code attributes use common underscore convention
|
file | diff | annotate |
| 2009-06-02 |
haftmann |
2009-06-02 |
OCaml builtin intergers are elusive; avoid
|
file | diff | annotate |
| 2009-05-27 |
haftmann |
2009-05-27 |
added lemma about 0 - 1
|
file | diff | annotate |
| 2009-05-19 |
haftmann |
2009-05-19 |
String.literal replaces message_string, code_numeral replaces (code_)index
|
file | diff | annotate | base |