src/HOL/Imperative_HOL/Heap_Monad.thy
2010-09-01 haftmann 2010-09-01 Graph.map, in analogy to Table.map
2010-09-01 haftmann 2010-09-01 do not print object frame around Scala includes -- this is in the responsibility of the user
2010-08-26 haftmann 2010-08-26 prevent line breaks after Scala symbolic operators
2010-08-26 haftmann 2010-08-26 code_include Scala: qualify module nmae
2010-08-13 haftmann 2010-08-13 lemma execute_bind_case
2010-08-12 haftmann 2010-08-12 tuned
2010-08-12 haftmann 2010-08-12 tuned
2010-07-29 haftmann 2010-07-29 proper unit type in transformed program
2010-07-26 haftmann 2010-07-26 use Natural as index type for Haskell and Scala
2010-07-23 haftmann 2010-07-23 avoid unreliable Haskell Int type
2010-07-19 haftmann 2010-07-19 dropped superfluous prefixes
2010-07-16 haftmann 2010-07-16 first roughly working version of Imperative HOL for Scala
2010-07-16 haftmann 2010-07-16 a first sketch for Imperative HOL witht Scala
2010-07-16 haftmann 2010-07-16 fragments of Scala
2010-07-15 haftmann 2010-07-15 dropped spurious export_code
2010-07-14 haftmann 2010-07-14 repaired some implementations of imperative operations
2010-07-14 haftmann 2010-07-14 avoid ambiguities; tuned
2010-07-14 haftmann 2010-07-14 dropped M suffix; added predicate monad bind
2010-07-13 krauss 2010-07-13 Heap_Monad uses Monad_Syntax
2010-07-13 haftmann 2010-07-13 theorem collections do not contain default rules any longer
2010-07-12 haftmann 2010-07-12 split off mrec into separate theory
2010-07-12 haftmann 2010-07-12 spelt out relational framework in a consistent way
2010-07-09 haftmann 2010-07-09 pervasive success combinator
2010-07-09 haftmann 2010-07-09 avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
2010-07-09 haftmann 2010-07-09 guard combinator
2010-07-06 haftmann 2010-07-06 tuned
2010-07-05 haftmann 2010-07-05 simplified representation of monad type
2010-06-28 haftmann 2010-06-28 merged constants "split" and "prod_case"
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;
2010-04-06 krauss 2010-04-06 removed (latex output) notation which is sometimes very ugly
2010-03-31 bulwahn 2010-03-31 adding MREC induction rule in Imperative HOL
2010-03-01 wenzelm 2010-03-01 eliminated hard tabs;
2010-02-11 wenzelm 2010-02-11 modernized translations; formal markup of @{syntax_const} and @{const_syntax};
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