src/HOL/Imperative_HOL/Array.thy
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
2010-11-22 haftmann 2010-11-22 renamed slightly ambivalent crel to effect
2010-11-04 haftmann 2010-11-04 added lemma length_alloc
2010-09-27 haftmann 2010-09-27 treat equality on refs and arrays as primitive operation
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-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 do not print object frame around Scala includes -- this is in the responsibility of the user
2010-08-26 haftmann 2010-08-26 code_include Scala: qualify module nmae
2010-07-26 haftmann 2010-07-26 use Natural as index type for Haskell and Scala
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-14 haftmann 2010-07-14 repaired some implementations of imperative operations
2010-07-14 haftmann 2010-07-14 repaired of_list implementation for SML, OCaml
2010-07-13 haftmann 2010-07-13 consolidated names of theorems
2010-07-13 haftmann 2010-07-13 qualified names for (really) all array operations
2010-07-13 haftmann 2010-07-13 canonical argument order for get
2010-07-13 haftmann 2010-07-13 qualified names for (almost) all array operations
2010-07-13 haftmann 2010-07-13 canonical argument order for present
2010-07-13 haftmann 2010-07-13 canonical argument order for length
2010-07-13 haftmann 2010-07-13 proper merge of operation changes and generic do-syntax
2010-07-13 haftmann 2010-07-13 merged
2010-07-13 haftmann 2010-07-13 hide_const; update replaces change
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 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 tuned array theory
2010-07-05 haftmann 2010-07-05 moved "open" operations from Heap.thy to Array.thy and Ref.thy
2010-07-05 haftmann 2010-07-05 remove primitive operation Heap.array in favour of Heap.array_of_list
2010-07-05 haftmann 2010-07-05 simplified representation of monad type
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-03-21 haftmann 2010-03-21 corrected setup for of_list
2009-09-15 haftmann 2009-09-15 restored code generation for OCaml
2009-06-30 haftmann 2009-06-30 dropped id
2009-05-19 haftmann 2009-05-19 String.literal replaces message_string, code_numeral replaces (code_)index
2009-05-19 haftmann 2009-05-19 moved Code_Index, Random and Quickcheck before Main
2009-02-06 haftmann 2009-02-06 authentic syntax for List.nth
2009-02-06 haftmann 2009-02-06 mandatory prefix for index conversion operations
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