2010-02-17 huffman 2010-02-17 add theory HOLCF/ex/Strict_Fun.thy
2010-02-17 haftmann 2010-02-17 tuned primrec signature: return definienda
2010-02-17 haftmann 2010-02-17 merged
2010-02-17 haftmann 2010-02-17 example for executable choice
2010-02-17 haftmann 2010-02-17 added simple theory about discrete summation
2010-02-17 wenzelm 2010-02-17 giving up sunbroy2;
2010-02-17 haftmann 2010-02-17 merged
2010-02-17 haftmann 2010-02-17 a draft for an example how to turn specifications involving choice executable
2010-02-17 haftmann 2010-02-17 added lemma map_of_map_restrict; generalized lemma dom_const
2010-02-17 haftmann 2010-02-17 adjusted to changes in theory Mapping
2010-02-17 haftmann 2010-02-17 more close integration with theory Map
2010-02-17 haftmann 2010-02-17 mappings implemented by association lists
2010-02-16 wenzelm 2010-02-16 merged
2010-02-16 boehmes 2010-02-16 updated SMT certificates
2010-02-16 boehmes 2010-02-16 include solver arguments as comments in SMT problem files (to distinguish different results from the same problem when caching results)
2010-02-16 boehmes 2010-02-16 updated SMT certificates
2010-02-16 boehmes 2010-02-16 added Cache_IO: cache for output of external tools, changed SMT solver interface to use Cache_IO
2010-02-16 hoelzl 2010-02-16 Rename transp to transpose in HOL-Multivariate_Analysis. (by himmelma)
2010-02-16 wenzelm 2010-02-16 simplified/clarified record print translations;
2010-02-16 wenzelm 2010-02-16 eliminated camel case;
2010-02-16 wenzelm 2010-02-16 tuned;
2010-02-16 wenzelm 2010-02-16 simplified/clarified record translations;
2010-02-16 wenzelm 2010-02-16 moved generic update_name to Pure syntax -- not specific to HOL/record;
2010-02-16 wenzelm 2010-02-16 tuned;
2010-02-16 wenzelm 2010-02-16 comment;
2010-02-16 wenzelm 2010-02-16 conceal internal record definitions;
2010-02-16 wenzelm 2010-02-16 simplified meaning of ProofContext.verbose; eliminated strange ProofContext.setmp_verbose_CRITICAL; less confusing printing of (cumulative) unnamed facts;
2010-02-16 wenzelm 2010-02-16 refrain from using @{const_name} in syntax translations;
2010-02-16 wenzelm 2010-02-16 misc tuning and simplification;
2010-02-15 wenzelm 2010-02-15 refined and exported record_info;
2010-02-15 wenzelm 2010-02-15 modernized structures;
2010-02-15 wenzelm 2010-02-15 modernized signature -- proper binding; misc tuning;
2010-02-15 wenzelm 2010-02-15 tuned errors; tuned;
2010-02-15 wenzelm 2010-02-15 Typedef.the_info;
2010-02-15 wenzelm 2010-02-15 formal markup of constants; misc tuning;
2010-02-15 wenzelm 2010-02-15 tuned document;
2010-02-15 wenzelm 2010-02-15 eliminated old fold;
2010-02-15 wenzelm 2010-02-15 renamed InfixName to Infix etc.;
2010-02-15 wenzelm 2010-02-15 discontinued unnamed infix syntax;
2010-02-15 wenzelm 2010-02-15 eliminated unnamed infixes;
2010-02-15 haftmann 2010-02-15 apply global morphism for theory, instantiation and overloading target; n.b. target morphism and global morphism coincide for theory target
2010-02-15 haftmann 2010-02-15 clarifed type
2010-02-14 boehmes 2010-02-14 optionally localize assertion labels (based on user-defined offsets) to reduce the effort of label adaptions after changes to the source program
2010-02-14 wenzelm 2010-02-14 formal markup of constants;
2010-02-13 wenzelm 2010-02-13 modernized structures;
2010-02-13 wenzelm 2010-02-13 authentic proof syntax;
2010-02-12 haftmann 2010-02-12 tuned import order
2010-02-12 haftmann 2010-02-12 tuned comments
2010-02-11 wenzelm 2010-02-11 merged
2010-02-11 huffman 2010-02-11 merged
2010-02-11 huffman 2010-02-11 change generated lemmas dist_eqs and dist_les to iff-style
2010-02-11 boehmes 2010-02-11 unfold quantifiers (Ball, Bex, Ex1)
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
2010-02-11 wenzelm 2010-02-11 formal markup of @{syntax_const} and @{const_syntax}; authentic syntax for extra robustness;
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax};
2010-02-11 wenzelm 2010-02-11 numeral syntax: clarify parse trees vs. actual terms; modernized translations; formal markup of @{syntax_const} and @{const_syntax};
2010-02-11 wenzelm 2010-02-11 added ML antiquotation @{syntax_const};
2010-02-11 wenzelm 2010-02-11 treat inner token markers as syntax consts;
2010-02-11 wenzelm 2010-02-11 modernized syntax/translations;
2010-02-11 wenzelm 2010-02-11 modernized syntax/translations; tuned headers;