author | paulson |
Thu, 01 Oct 1998 18:30:05 +0200 | |
changeset 5601 | b6456ccd9e3e |
parent 5261 | ce3c25c8a694 |
child 9762 | 66f7eefb3967 |
permissions | -rw-r--r-- |
5261 | 1 |
(* Title: HOL/Lambda/ListBeta.thy |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow |
|
4 |
Copyright 1998 TU Muenchen |
|
5 |
||
6 |
Lifting beta-reduction to lists of terms, reducing exactly one element |
|
7 |
*) |
|
8 |
||
9 |
ListBeta = ListApplication + ListOrder + |
|
10 |
||
11 |
syntax "=>" :: dB => dB => bool (infixl 50) |
|
12 |
translations "rs => ss" == "(rs,ss) : step1 beta" |
|
13 |
||
14 |
end |