| author | paulson |
| Thu, 20 Aug 1998 16:20:17 +0200 | |
| changeset 5349 | eab069aa1ad0 |
| 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