--- a/src/HOL/UNITY/Channel.ML Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/Channel.ML Thu Oct 15 11:35:07 1998 +0200
@@ -8,8 +8,6 @@
From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
*)
-AddIffs [skip];
-
(*None represents "infinity" while Some represents proper integers*)
Goalw [minSet_def] "minSet A = Some x --> x : A";
by (Simp_tac 1);
@@ -26,7 +24,7 @@
by (Blast_tac 1);
qed_spec_mp "minSet_nonempty";
-Goal "leadsTo acts (minSet -`` {Some x}) (minSet -`` (Some``greaterThan x))";
+Goal "F : leadsTo (minSet -`` {Some x}) (minSet -`` (Some``greaterThan x))";
by (rtac leadsTo_weaken 1);
by (rtac ([UC2, UC1] MRS psp) 1);
by (ALLGOALS Asm_simp_tac);
@@ -38,7 +36,7 @@
(*The induction*)
-Goal "leadsTo acts (UNIV-{{}}) (minSet -`` (Some``atLeast y))";
+Goal "F : leadsTo (UNIV-{{}}) (minSet -`` (Some``atLeast y))";
by (rtac leadsTo_weaken_R 1);
by (res_inst_tac [("l", "y"), ("f", "the o minSet"), ("B", "{}")]
greaterThan_bounded_induct 1);
@@ -54,7 +52,7 @@
val lemma = result();
-Goal "!!y::nat. leadsTo acts (UNIV-{{}}) {s. y ~: s}";
+Goal "!!y::nat. F : leadsTo (UNIV-{{}}) {s. y ~: s}";
by (rtac (lemma RS leadsTo_weaken_R) 1);
by (Clarify_tac 1);
by (forward_tac [minSet_nonempty] 1);