tr is (again) type abbrev;
authorwenzelm
Tue Mar 11 14:21:10 1997 +0100 (1997-03-11)
changeset 27825e8771682c73
parent 2781 0d6fcae3ae45
child 2783 7d0ec11966d4
tr is (again) type abbrev;
src/HOLCF/Tr.thy
     1.1 --- a/src/HOLCF/Tr.thy	Tue Mar 11 13:05:40 1997 +0100
     1.2 +++ b/src/HOLCF/Tr.thy	Tue Mar 11 14:21:10 1997 +0100
     1.3 @@ -8,10 +8,11 @@
     1.4  
     1.5  Tr = Lift +
     1.6  
     1.7 -syntax
     1.8 -  tr	:: "type"
     1.9 +types
    1.10 +  tr = "bool lift"
    1.11 +
    1.12  translations
    1.13 -  "tr" == (type) "bool lift" 
    1.14 +  "tr" <= (type) "bool lift" 
    1.15  
    1.16  consts
    1.17  	TT,FF           :: "tr"