# HG changeset patch
# User wenzelm
# Date 858086470 -3600
# Node ID 5e8771682c73f953ed80e5cbe6abaca24a4847b7
# Parent  0d6fcae3ae45565033b0d2550e96eefebe123ffe
tr is (again) type abbrev;

diff -r 0d6fcae3ae45 -r 5e8771682c73 src/HOLCF/Tr.thy
--- a/src/HOLCF/Tr.thy	Tue Mar 11 13:05:40 1997 +0100
+++ b/src/HOLCF/Tr.thy	Tue Mar 11 14:21:10 1997 +0100
@@ -8,10 +8,11 @@
 
 Tr = Lift +
 
-syntax
-  tr	:: "type"
+types
+  tr = "bool lift"
+
 translations
-  "tr" == (type) "bool lift" 
+  "tr" <= (type) "bool lift" 
 
 consts
 	TT,FF           :: "tr"