src/HOL/ex/Tarski.thy

--- a/src/HOL/ex/Tarski.thy	Fri Jan 05 18:33:47 2001 +0100
+++ b/src/HOL/ex/Tarski.thy	Fri Jan 05 18:48:18 2001 +0100
@@ -94,7 +94,7 @@
   "@SL"  :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
 
 translations
-  "S <<= cl" == "S : sublattice ^^ {cl}"
+  "S <<= cl" == "S : sublattice ``` {cl}"
 
 constdefs
   dual :: "'a potype => 'a potype"
@@ -121,7 +121,7 @@
   f :: "'a => 'a"
   P :: "'a set"
 assumes 
-  f_cl "f : CLF ^^{cl}"
+  f_cl "f : CLF```{cl}"
 defines
   P_def "P == fix f A"