src/HOLCF/Tr.thy
changeset 2766 3e90c5187ce1
parent 2719 27167b432e7a
child 2782 5e8771682c73
--- 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