--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/example.ML Wed Mar 04 11:05:02 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-structure Example =
-struct
-
-fun foldl f a [] = a
- | foldl f a (x :: xs) = foldl f (f a x) xs;
-
-fun rev xs = foldl (fn xsa => fn x => x :: xsa) [] xs;
-
-fun list_case f1 f2 (a :: lista) = f2 a lista
- | list_case f1 f2 [] = f1;
-
-datatype 'a queue = AQueue of 'a list * 'a list;
-
-val empty : 'a queue = AQueue ([], [])
-
-fun dequeue (AQueue ([], [])) = (NONE, AQueue ([], []))
- | dequeue (AQueue (xs, y :: ys)) = (SOME y, AQueue (xs, ys))
- | dequeue (AQueue (v :: va, [])) =
- let
- val y :: ys = rev (v :: va);
- in
- (SOME y, AQueue ([], ys))
- end;
-
-fun enqueue x (AQueue (xs, ys)) = AQueue (x :: xs, ys);
-
-end; (*struct Example*)