diff -r c0bcea781b3a -r 028d22926a41 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Fri Jan 05 18:33:47 2001 +0100
+++ b/src/HOL/Integ/IntDef.thy	Fri Jan 05 18:48:18 2001 +0100
@@ -19,12 +19,12 @@
 
 defs
   zminus_def
-    "- Z == Abs_Integ(UN (x,y):Rep_Integ(Z). intrel^^{(y,x)})"
+    "- Z == Abs_Integ(UN (x,y):Rep_Integ(Z). intrel```{(y,x)})"
 
 constdefs
 
   int :: nat => int
-  "int m == Abs_Integ(intrel ^^ {(m,0)})"
+  "int m == Abs_Integ(intrel ``` {(m,0)})"
 
   neg   :: int => bool
   "neg(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)"
@@ -40,7 +40,7 @@
   zadd_def
    "z + w == 
        Abs_Integ(UN (x1,y1):Rep_Integ(z). UN (x2,y2):Rep_Integ(w).   
-		 intrel^^{(x1+x2, y1+y2)})"
+		 intrel```{(x1+x2, y1+y2)})"
 
   zdiff_def "z - (w::int) == z + (-w)"
 
@@ -51,6 +51,6 @@
   zmult_def
    "z * w == 
        Abs_Integ(UN (x1,y1):Rep_Integ(z). UN (x2,y2):Rep_Integ(w).   
-		 intrel^^{(x1*x2 + y1*y2, x1*y2 + y1*x2)})"
+		 intrel```{(x1*x2 + y1*y2, x1*y2 + y1*x2)})"
 
 end