--- a/doc-src/Tutorial/Misc/Last.thy Mon Nov 29 11:18:16 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-Last = List +
-consts last :: 'a list => 'a
-recdef last "measure (%xs. length xs)"
- "last [x] = x"
- "last (x#y#zs) = last (y#zs)"
-end