--- a/src/HOL/UNITY/FP.ML Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/UNITY/FP.ML Tue Jan 09 15:32:27 2001 +0100
@@ -49,11 +49,11 @@
qed "FP_weakest";
Goalw [FP_def, stable_def, constrains_def]
- "-(FP F) = (UN act: Acts F. -{s. act```{s} <= {s}})";
+ "-(FP F) = (UN act: Acts F. -{s. act``{s} <= {s}})";
by (Blast_tac 1);
qed "Compl_FP";
-Goal "A - (FP F) = (UN act: Acts F. A - {s. act```{s} <= {s}})";
+Goal "A - (FP F) = (UN act: Acts F. A - {s. act``{s} <= {s}})";
by (simp_tac (simpset() addsimps [Diff_eq, Compl_FP]) 1);
qed "Diff_FP";