src/HOL/Imperative_HOL/Heap_Monad.thy
2014-12-05 haftmann 2014-12-05 allow multiple inheritance of targets
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-22 wenzelm 2014-11-22 named_theorems: multiple args;
2014-11-08 haftmann 2014-11-08 less space-wasting serialization setup: highest cell of array has been unused so far
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-02 haftmann 2014-10-02 tuned Heap_Monad.successE
2014-09-18 haftmann 2014-09-18 tuned data structure
2014-09-11 blanchet 2014-09-11 updated news
2014-09-09 blanchet 2014-09-09 use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
2014-08-16 wenzelm 2014-08-16 updated to named_theorems;
2014-06-30 haftmann 2014-06-30 qualified String.explode and String.implode
2014-02-09 haftmann 2014-02-09 dropped legacy finally
2014-01-25 haftmann 2014-01-25 prefer explicit code symbol type over ad-hoc name mangling
2013-12-05 Andreas Lochbihler 2013-12-05 restrict admissibility to non-empty chains to allow more syntax-directed proof rules
2013-09-02 Andreas Lochbihler 2013-09-02 move admissible out of class ccpo to avoid unnecessary class predicate in foundational theorems
2013-07-24 krauss 2013-07-24 derive specialized version of full fixpoint induction (with admissibility)
2013-07-12 wenzelm 2013-07-12 localized and modernized adhoc-overloading (patch by Christian Sternagel);
2013-06-23 haftmann 2013-06-23 migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
2013-06-18 lammich 2013-06-18 Added parantheses to code_type for heap monad
2013-03-22 krauss 2013-03-22 added rudimentary induction rule for partial_function (heap)
2013-02-15 haftmann 2013-02-15 two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
2012-06-05 haftmann 2012-06-05 prefer sys.error over plain error in Scala to avoid deprecation warning
2012-06-05 haftmann 2012-06-05 prefer records with speaking labels over deeply nested tuples
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