src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
2010-07-05 ago moved "open" operations from Heap.thy to Array.thy and Ref.thy
2010-04-16 ago replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
2010-04-08 ago added imperative SAT checker; improved headers of example files; adopted IsaMakefile
2009-12-10 ago added Imperative_HOL examples; added tail-recursive combinator for monadic heap functions; adopted code generation of references; added lemmas