src/HOL/UNITY/UNITY.ML

 by (Blast_tac 1);
 qed "Int_Union_Union";
 
 (** Needed for WF reasoning in WFair.ML **)
 
-Goal "less_than ^^ {k} = greaterThan k";
+Goal "less_than ``` {k} = greaterThan k";
 by (Blast_tac 1);
 qed "Image_less_than";
 
-Goal "less_than^-1 ^^ {k} = lessThan k";
+Goal "less_than^-1 ``` {k} = lessThan k";
 by (Blast_tac 1);
 qed "Image_inverse_less_than";
 
 Addsimps [Image_less_than, Image_inverse_less_than];