| Mon, 22 Nov 2010 09:37:39 +0100 |
haftmann |
renamed slightly ambivalent crel to effect
|
file |
diff |
annotate
|
| Thu, 04 Nov 2010 17:27:37 +0100 |
haftmann |
added lemma length_alloc
|
file |
diff |
annotate
|
| Mon, 27 Sep 2010 11:12:01 +0200 |
haftmann |
treat equality on refs and arrays as primitive operation
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 11:09:50 +0200 |
haftmann |
do not print object frame around Scala includes -- this is in the responsibility of the user
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 10:16:22 +0200 |
haftmann |
code_include Scala: qualify module nmae
|
file |
diff |
annotate
|
| Mon, 26 Jul 2010 11:09:44 +0200 |
haftmann |
use Natural as index type for Haskell and Scala
|
file |
diff |
annotate
|
| Fri, 16 Jul 2010 15:28:22 +0200 |
haftmann |
first roughly working version of Imperative HOL for Scala
|
file |
diff |
annotate
|
| Fri, 16 Jul 2010 13:58:29 +0200 |
haftmann |
a first sketch for Imperative HOL witht Scala
|
file |
diff |
annotate
|
| Wed, 14 Jul 2010 17:15:58 +0200 |
haftmann |
repaired some implementations of imperative operations
|
file |
diff |
annotate
|
| Wed, 14 Jul 2010 16:45:29 +0200 |
haftmann |
repaired of_list implementation for SML, OCaml
|
file |
diff |
annotate
|
| Tue, 13 Jul 2010 16:30:13 +0200 |
haftmann |
consolidated names of theorems
|
file |
diff |
annotate
|
| Tue, 13 Jul 2010 16:21:49 +0200 |
haftmann |
qualified names for (really) all array operations
|
file |
diff |
annotate
|
| Tue, 13 Jul 2010 16:12:40 +0200 |
haftmann |
canonical argument order for get
|
file |
diff |
annotate
|
| Tue, 13 Jul 2010 16:00:56 +0200 |
haftmann |
qualified names for (almost) all array operations
|
file |
diff |
annotate
|
| Tue, 13 Jul 2010 15:37:31 +0200 |
haftmann |
canonical argument order for present
|
file |
diff |
annotate
|
| Tue, 13 Jul 2010 15:34:02 +0200 |
haftmann |
canonical argument order for length
|
file |
diff |
annotate
|
| Tue, 13 Jul 2010 12:16:24 +0200 |
haftmann |
proper merge of operation changes and generic do-syntax
|
file |
diff |
annotate
|
| Tue, 13 Jul 2010 12:05:20 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Tue, 13 Jul 2010 12:01:34 +0200 |
haftmann |
hide_const; update replaces change
|
file |
diff |
annotate
|
| Tue, 13 Jul 2010 12:00:11 +0200 |
krauss |
Heap_Monad uses Monad_Syntax
|
file |
diff |
annotate
|
| Tue, 13 Jul 2010 11:38:03 +0200 |
haftmann |
theorem collections do not contain default rules any longer
|
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:52 +0200 |
haftmann |
tuned array theory
|
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: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
|