--- a/src/HOL/UNITY/Common.ML Tue Sep 15 13:09:23 1998 +0200
+++ b/src/HOL/UNITY/Common.ML Tue Sep 15 15:04:07 1998 +0200
@@ -79,9 +79,9 @@
addIs [common_stable, LeadsTo_weaken_R]) 1);
val lemma = result();
-(*The "ALL m: Compl common" form echoes CMT6.*)
+(*The "ALL m: -common" form echoes CMT6.*)
Goal "[| ALL m. Constrains prg {m} (maxfg m); \
-\ ALL m: Compl common. LeadsTo prg {m} (greaterThan m); \
+\ ALL m: -common. LeadsTo prg {m} (greaterThan m); \
\ n: common; id: Acts prg |] \
\ ==> LeadsTo prg (atMost (LEAST n. n: common)) common";
by (rtac lemma 1);