src/HOL/Imperative_HOL/Heap.thy
2010-12-29 wenzelm 2010-12-29 explicit file specifications -- avoid secondary load path;
2010-09-09 bulwahn 2010-09-09 changing String.literal to a type instead of a datatype
2010-08-13 haftmann 2010-08-13 unit and bool are instances of heap
2010-07-06 haftmann 2010-07-06 tuned empty heap
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 only definite assignment
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 tuned
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-05-04 bulwahn 2010-05-04 added lemma about irreflexivity of pointer inequality in Imperative_HOL
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;
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-11-12 hoelzl 2009-11-12 New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
2009-05-19 haftmann 2009-05-19 String.literal replaces message_string, code_numeral replaces (code_)index
2009-03-27 haftmann 2009-03-27 normalized imports
2009-01-08 haftmann 2009-01-08 split of Imperative_HOL theories from HOL-Library