src/HOL/Imperative_HOL/Ref.thy
2010-08-26 haftmann 2010-08-26 code_include Scala: qualify module nmae
2010-07-29 haftmann 2010-07-29 intermediate operation avoids invariance problem in Scala
2010-07-26 haftmann 2010-07-26 modified namespace policy
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-14 haftmann 2010-07-14 repaired reference implementation for OCaml
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 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 tuned reference theory
2010-07-06 haftmann 2010-07-06 refactored reference operations
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 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;
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-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