--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Lambda/ListBeta.thy	Thu Aug 06 10:33:54 1998 +0200
@@ -0,0 +1,14 @@
+(*  Title:      HOL/Lambda/ListBeta.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   1998 TU Muenchen
+
+Lifting beta-reduction to lists of terms, reducing exactly one element
+*)
+
+ListBeta = ListApplication + ListOrder +
+
+syntax "=>" :: dB => dB => bool (infixl 50)
+translations "rs => ss" == "(rs,ss) : step1 beta"
+
+end