--- a/src/HOL/UNITY/Extend.ML Fri Jan 05 18:33:47 2001 +0100
+++ b/src/HOL/UNITY/Extend.ML Fri Jan 05 18:48:18 2001 +0100
@@ -58,7 +58,7 @@
by (Blast_tac 1);
qed "Domain_Restrict";
-Goal "(Restrict A r) ^^ B = r ^^ (A Int B)";
+Goal "(Restrict A r) ``` B = r ``` (A Int B)";
by (Blast_tac 1);
qed "Image_Restrict";
@@ -308,7 +308,7 @@
qed "inj_extend_act";
Goalw [extend_set_def, extend_act_def]
- "extend_act h act ^^ (extend_set h A) = extend_set h (act ^^ A)";
+ "extend_act h act ``` (extend_set h A) = extend_set h (act ``` A)";
by (Force_tac 1);
qed "extend_act_Image";
Addsimps [extend_act_Image];