2009-12-10 bulwahn 2009-12-10 added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas
2009-07-14 haftmann 2009-07-14 prefer code_inline over code_unfold; use code_unfold_post where appropriate
2009-07-14 haftmann 2009-07-14 code attributes use common underscore convention
2009-06-30 haftmann 2009-06-30 adaptated to changes in term representation
2009-06-30 haftmann 2009-06-30 streamlined code
2009-06-19 haftmann 2009-06-19 more appropriate syntax for IML abstraction
2009-05-19 haftmann 2009-05-19 String.literal replaces message_string, code_numeral replaces (code_)index
2009-05-07 haftmann 2009-05-07 explicit type arguments in constants
2009-02-03 haftmann 2009-02-03 changed name space policy for Haskell includes
2009-01-08 haftmann 2009-01-08 split of Imperative_HOL theories from HOL-Library