src/HOL/Imperative_HOL/Heap_Monad.thy
2011-12-29 haftmann 2011-12-29 attribute code_abbrev superseedes code_unfold_post; tuned names and spacing
2011-10-28 wenzelm 2011-10-28 tuned Named_Thms: proper binding;
2011-10-21 bulwahn 2011-10-21 replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
2011-09-07 bulwahn 2011-09-07 adapting Imperative HOL serializer to changes of the iterm datatype in the code generator
2011-08-12 huffman 2011-08-12 make more HOL theories work with separate set type
2011-06-09 wenzelm 2011-06-09 discontinued Name.variant to emphasize that this is old-style / indirect;
2011-05-23 krauss 2011-05-23 also manage induction rule; tuned data slot
2011-05-23 krauss 2011-05-23 separate initializations for different modes of partial_function -- generation of induction rules will be non-uniform
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-11-22 haftmann 2010-11-22 renamed slightly ambivalent crel to effect
2010-10-29 haftmann 2010-10-29 tuned structure of theory
2010-10-29 haftmann 2010-10-29 remove term_of equations for Heap type explicitly
2010-10-26 krauss 2010-10-26 added Heap monad instance of partial_function package
2010-09-13 nipkow 2010-09-13 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
2010-09-09 bulwahn 2010-09-09 changing String.literal to a type instead of a datatype
2010-09-07 nipkow 2010-09-07 expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
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