src/HOL/Imperative_HOL/Array.thy
Tue, 13 Jul 2010 16:00:56 +0200 haftmann qualified names for (almost) all array operations
Tue, 13 Jul 2010 15:37:31 +0200 haftmann canonical argument order for present
Tue, 13 Jul 2010 15:34:02 +0200 haftmann canonical argument order for length
Tue, 13 Jul 2010 12:16:24 +0200 haftmann proper merge of operation changes and generic do-syntax
Tue, 13 Jul 2010 12:05:20 +0200 haftmann merged
Tue, 13 Jul 2010 12:01:34 +0200 haftmann hide_const; update replaces change
Tue, 13 Jul 2010 12:00:11 +0200 krauss Heap_Monad uses Monad_Syntax
Tue, 13 Jul 2010 11:38:03 +0200 haftmann theorem collections do not contain default rules any longer
Mon, 12 Jul 2010 16:05:08 +0200 haftmann spelt out relational framework in a consistent way
Fri, 09 Jul 2010 16:58:44 +0200 haftmann pervasive success combinator
Fri, 09 Jul 2010 10:08:10 +0200 haftmann avoid slightly odd "M" suffix; rename mapM to fold_map (fold_map_abort would be more correct, though)
Fri, 09 Jul 2010 09:48:52 +0200 haftmann tuned array theory
Mon, 05 Jul 2010 16:46:23 +0200 haftmann moved "open" operations from Heap.thy to Array.thy and Ref.thy
Mon, 05 Jul 2010 15:25:42 +0200 haftmann remove primitive operation Heap.array in favour of Heap.array_of_list
Mon, 05 Jul 2010 14:34:28 +0200 haftmann simplified representation of monad type
less more (0) -15 tip