| author | wenzelm |
| Tue, 04 May 1999 18:55:43 +0200 | |
| changeset 6585 | d5eae11efa42 |
| parent 5261 | ce3c25c8a694 |
| child 9762 | 66f7eefb3967 |
| permissions | -rw-r--r-- |
(* 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