2014-09-11 |
blanchet |
updated news
|
file |
diff |
annotate
|
2014-09-02 |
blanchet |
use 'datatype_new' in 'Main'
|
file |
diff |
annotate
|
2014-07-04 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
2014-06-30 |
haftmann |
qualified String.explode and String.implode
|
file |
diff |
annotate
|
2014-06-12 |
nipkow |
added [simp]
|
file |
diff |
annotate
|
2014-05-04 |
blanchet |
renamed 'xxx_size' to 'size_xxx' for old datatype package
|
file |
diff |
annotate
|
2014-03-07 |
blanchet |
use balanced tuples in 'primcorec'
|
file |
diff |
annotate
|
2014-02-20 |
blanchet |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
file |
diff |
annotate
|
2014-02-12 |
Andreas Lochbihler |
merged
|
file |
diff |
annotate
|
2014-02-12 |
Andreas Lochbihler |
make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
|
file |
diff |
annotate
|
2014-02-12 |
blanchet |
adapted theories to 'xxx_case' to 'case_xxx'
|
file |
diff |
annotate
|
2014-01-15 |
wenzelm |
added \<newline> symbol, which is used for char/string literals in HOL;
|
file |
diff |
annotate
|
2013-11-20 |
Andreas Lochbihler |
setup lifting/transfer for String.literal
|
file |
diff |
annotate
|
2013-10-09 |
Andreas Lochbihler |
add congruence rule to prevent code_simp from looping
|
file |
diff |
annotate
|
2013-08-08 |
Andreas Lochbihler |
abort execution of generated code with explicit exception message
|
file |
diff |
annotate
|
2013-06-23 |
haftmann |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
|
file |
diff |
annotate
|
2013-06-11 |
haftmann |
reflexive nbe equation for equality on String.literal
|
file |
diff |
annotate
|
2013-04-18 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
2013-02-15 |
haftmann |
systematic conversions between nat and nibble/char;
|
file |
diff |
annotate
|
2012-10-22 |
haftmann |
incorporated constant chars into instantiation proof for enum;
|
file |
diff |
annotate
|
2012-10-20 |
haftmann |
moved quite generic material from theory Enum to more appropriate places
|
file |
diff |
annotate
|
2012-10-12 |
wenzelm |
discontinued obsolete typedef (open) syntax;
|
file |
diff |
annotate
|
2012-08-22 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
2012-02-15 |
wenzelm |
renamed "xstr" to "str_token";
|
file |
diff |
annotate
|
2011-11-14 |
wenzelm |
inner syntax positions for string literals;
|
file |
diff |
annotate
|
2011-10-19 |
bulwahn |
removing old code generator setup for strings
|
file |
diff |
annotate
|
2011-08-18 |
haftmann |
observe distinction between sets and predicates more properly
|
file |
diff |
annotate
|
2011-04-21 |
wenzelm |
discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;
|
file |
diff |
annotate
|
2011-04-19 |
wenzelm |
eliminated Codegen.mode in favour of explicit argument;
|
file |
diff |
annotate
|
2011-03-30 |
bulwahn |
renewing specifications in HOL: replacing types by type_synonym
|
file |
diff |
annotate
|
2011-02-10 |
haftmann |
reverted cs. 0a3fa8fbcdc5 -- motivation is unreconstructable, produces confusion in user space
|
file |
diff |
annotate
|
2010-09-20 |
wenzelm |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file |
diff |
annotate
|
2010-09-13 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
2010-09-10 |
bulwahn |
fiddling with the correct setup for String.literal
|
file |
diff |
annotate
|
2010-09-10 |
haftmann |
Haskell == is infix, not infixl
|
file |
diff |
annotate
|
2010-09-09 |
bulwahn |
changing String.literal to a type instead of a datatype
|
file |
diff |
annotate
|
2010-09-07 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
2010-08-28 |
haftmann |
merged
|
file |
diff |
annotate
|
2010-08-27 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|
2010-08-27 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
2010-07-08 |
haftmann |
tuned module names
|
file |
diff |
annotate
|
2010-04-16 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file |
diff |
annotate
|
2010-02-13 |
wenzelm |
modernized structures;
|
file |
diff |
annotate
|
2010-02-11 |
wenzelm |
modernized translations;
|
file |
diff |
annotate
|
2010-01-13 |
haftmann |
some syntax setup for Scala
|
file |
diff |
annotate
|
2009-10-27 |
haftmann |
tuned
|
file |
diff |
annotate
|
2009-10-22 |
haftmann |
map_range (and map_index) combinator
|
file |
diff |
annotate
|
2009-07-14 |
haftmann |
prefer code_inline over code_unfold; use code_unfold_post where appropriate
|
file |
diff |
annotate
|
2009-07-14 |
haftmann |
code attributes use common underscore convention
|
file |
diff |
annotate
|
2009-06-08 |
haftmann |
constant "chars" of all characters
|
file |
diff |
annotate
|
2009-05-19 |
haftmann |
String.literal replaces message_string, code_numeral replaces (code_)index
|
file |
diff |
annotate
|
2009-05-17 |
haftmann |
is a definition
|
file |
diff |
annotate
|
2009-05-16 |
bulwahn |
added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
|
file |
diff |
annotate
|
2009-05-06 |
haftmann |
proper structures for list and string code generation stuff
|
file |
diff |
annotate
|
2009-05-06 |
haftmann |
refined HOL string theories and corresponding ML fragments
|
file |
diff |
annotate
|
2001-01-15 |
wenzelm |
improved string syntax (allow translation rules);
|
file |
diff |
annotate
|
2000-12-23 |
wenzelm |
Tools/string_syntax.ML;
|
file |
diff |
annotate
|
1999-08-16 |
wenzelm |
'a list: Nil, Cons;
|
file |
diff |
annotate
|
1999-03-17 |
wenzelm |
xstr token class;
|
file |
diff |
annotate
|
1998-07-03 |
wenzelm |
moved String theory to main HOL;
|
file |
diff |
annotate
|