| Mon, 12 Jul 2010 16:26:48 +0200 |
haftmann |
dropped unused lemmas of dubious value
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 16:23:30 +0200 |
haftmann |
dropped unused lemmas of dubious value
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 16:19:15 +0200 |
haftmann |
split off mrec into separate theory
|
file |
diff |
annotate
|
| Mon, 12 Jul 2010 16:05:08 +0200 |
haftmann |
spelt out relational framework in a consistent way
|
file |
diff |
annotate
|
| Fri, 09 Jul 2010 16:58:44 +0200 |
haftmann |
pervasive success combinator
|
file |
diff |
annotate
|
| 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)
|
file |
diff |
annotate
|
| Fri, 09 Jul 2010 09:48:54 +0200 |
haftmann |
adapted to changes
|
file |
diff |
annotate
|
| Tue, 06 Jul 2010 09:21:15 +0200 |
haftmann |
refactored reference operations
|
file |
diff |
annotate
|
| Mon, 05 Jul 2010 16:46:23 +0200 |
haftmann |
moved "open" operations from Heap.thy to Array.thy and Ref.thy
|
file |
diff |
annotate
|
| Mon, 05 Jul 2010 15:36:37 +0200 |
haftmann |
only definite assignment
|
file |
diff |
annotate
|
| Mon, 05 Jul 2010 15:25:42 +0200 |
haftmann |
remove primitive operation Heap.array in favour of Heap.array_of_list
|
file |
diff |
annotate
|
| Mon, 05 Jul 2010 14:34:28 +0200 |
haftmann |
simplified representation of monad type
|
file |
diff |
annotate
|
| Wed, 31 Mar 2010 16:44:41 +0200 |
bulwahn |
adding MREC induction rule in Imperative HOL
|
file |
diff |
annotate
|
| Thu, 08 Jan 2009 17:10:41 +0100 |
haftmann |
split of Imperative_HOL theories from HOL-Library
|
file |
diff |
annotate
| base
|