# HG changeset patch
# User wenzelm
# Date 857744902 -3600
# Node ID 3e90c5187ce11603f69ef481c1cd198af7ff8c7c
# Parent  a4afcfed261c6ce8706b39bfe3e33bb2271868aa
"bool lift" now syntax instead of type abbrev;

diff -r a4afcfed261c -r 3e90c5187ce1 src/HOLCF/Tr.thy
--- a/src/HOLCF/Tr.thy	Fri Mar 07 15:23:12 1997 +0100
+++ b/src/HOLCF/Tr.thy	Fri Mar 07 15:28:22 1997 +0100
@@ -8,7 +8,10 @@
 
 Tr = Lift +
 
-types tr = "bool lift"
+syntax
+  tr	:: "type"
+translations
+  "tr" == (type) "bool lift" 
 
 consts
 	TT,FF           :: "tr"
@@ -23,7 +26,6 @@
         "@orelse"       :: "tr => tr => tr" ("_ orelse _"  [31,30] 30)
  
 translations 
-	     "tr" ==(type) "bool lift" 
 	     "x andalso y" == "trand`x`y"
              "x orelse y"  == "tror`x`y"
              "If b then e1 else e2 fi" == "Icifte`b`e1`e2"
@@ -40,7 +42,7 @@
 *)
   plift_def   "plift p == (LAM x. flift1(%a.Def(p a))`x)"
 
-(* start 8bit 1 *)
+(* FIXME remove?
 syntax
   "GeqTT"        :: "tr => bool"               ("(\\<lceil>_\\<rceil>)")
   "GeqFF"        :: "tr => bool"               ("(\\<lfloor>_\\<rfloor>)")
@@ -48,7 +50,7 @@
 translations
   "\\<lceil>x\\<rceil>" == "x = TT"
   "\\<lfloor>x\\<rfloor>" == "x = FF"
-(* end 8bit 1 *)
+*)
 
 end