author | wenzelm |
Sun, 29 Nov 1998 13:16:47 +0100 | |
changeset 5989 | 9670dae0143d |
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