src/HOL/Imperative_HOL/Array.thy
2010-07-13 ago canonical argument order for get
2010-07-13 ago qualified names for (almost) all array operations
2010-07-13 ago canonical argument order for present
2010-07-13 ago canonical argument order for length
2010-07-13 ago proper merge of operation changes and generic do-syntax
2010-07-13 ago merged
2010-07-13 ago hide_const; update replaces change
2010-07-13 ago Heap_Monad uses Monad_Syntax
2010-07-13 ago theorem collections do not contain default rules any longer
2010-07-12 ago spelt out relational framework in a consistent way
2010-07-09 ago pervasive success combinator
2010-07-09 ago avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
2010-07-09 ago tuned array theory
2010-07-05 ago moved "open" operations from Heap.thy to Array.thy and Ref.thy
2010-07-05 ago remove primitive operation Heap.array in favour of Heap.array_of_list
2010-07-05 ago simplified representation of monad type
2010-04-16 ago replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-03-21 ago corrected setup for of_list
2009-09-15 ago restored code generation for OCaml
2009-06-30 ago dropped id
2009-05-19 ago String.literal replaces message_string, code_numeral replaces (code_)index
2009-05-19 ago moved Code_Index, Random and Quickcheck before Main
2009-02-06 ago authentic syntax for List.nth
2009-02-06 ago mandatory prefix for index conversion operations
2009-02-03 ago changed name space policy for Haskell includes
2009-01-08 ago split of Imperative_HOL theories from HOL-Library