--- a/src/HOL/UNITY/Deadlock.ML Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/UNITY/Deadlock.ML Mon Jun 22 17:26:46 1998 +0200
@@ -3,25 +3,25 @@
(*** Deadlock examples from section 5.6 ***)
(*Trivial, two-process case*)
-goalw thy [constrains_def, stable_def]
+Goalw [constrains_def, stable_def]
"!!Acts. [| constrains Acts (A Int B) A; constrains Acts (B Int A) B |] \
\ ==> stable Acts (A Int B)";
by (Blast_tac 1);
result();
-goal thy "{i. i < Suc n} = insert n {i. i < n}";
+Goal "{i. i < Suc n} = insert n {i. i < n}";
by (blast_tac (claset() addSEs [less_SucE] addIs [less_SucI]) 1);
qed "Collect_less_Suc_insert";
-goal thy "{i. i <= Suc n} = insert (Suc n) {i. i <= n}";
+Goal "{i. i <= Suc n} = insert (Suc n) {i. i <= n}";
by (blast_tac (claset() addSEs [le_SucE] addIs [le_SucI]) 1);
qed "Collect_le_Suc_insert";
(*a simplification step*)
-goal thy "(INT i:{i. i <= n}. A(Suc i) Int A i) = \
+Goal "(INT i:{i. i <= n}. A(Suc i) Int A i) = \
\ (INT i:{i. i <= Suc n}. A i)";
by (induct_tac "n" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Collect_le_Suc_insert])));
@@ -30,7 +30,7 @@
(*Dual of the required property. Converse inclusion fails.*)
-goal thy "(UN i:{i. i < n}. A i) Int Compl (A n) <= \
+Goal "(UN i:{i. i < n}. A i) Int Compl (A n) <= \
\ (UN i:{i. i < n}. (A i) Int Compl (A(Suc i)))";
by (induct_tac "n" 1);
by (Asm_simp_tac 1);
@@ -40,7 +40,7 @@
(*Converse inclusion fails.*)
-goal thy "(INT i:{i. i < n}. Compl(A i) Un A (Suc i)) <= \
+Goal "(INT i:{i. i < n}. Compl(A i) Un A (Suc i)) <= \
\ (INT i:{i. i < n}. Compl(A i)) Un A n";
by (induct_tac "n" 1);
by (Asm_simp_tac 1);
@@ -50,14 +50,14 @@
(*Specialized rewriting*)
-goal thy "A 0 Int (Compl (A n) Int \
+Goal "A 0 Int (Compl (A n) Int \
\ (INT i:{i. i < n}. Compl(A i) Un A (Suc i))) = {}";
by (blast_tac (claset() addIs [gr0I]
addDs [impOfSubs INT_Un_Compl_subset]) 1);
val lemma = result();
(*Reverse direction makes it harder to invoke the ind hyp*)
-goal thy "(INT i:{i. i <= n}. A i) = \
+Goal "(INT i:{i. i <= n}. A i) = \
\ A 0 Int (INT i:{i. i < n}. Compl(A i) Un A(Suc i))";
by (induct_tac "n" 1);
by (Asm_simp_tac 1);
@@ -67,7 +67,7 @@
Collect_less_Suc_insert, Collect_le_Suc_insert])) 1);
qed "INT_le_equals_Int";
-goal thy "(INT i:{i. i <= Suc n}. A i) = \
+Goal "(INT i:{i. i <= Suc n}. A i) = \
\ A 0 Int (INT i:{i. i <= n}. Compl(A i) Un A(Suc i))";
by (simp_tac (simpset() addsimps [le_eq_less_Suc RS sym,
INT_le_equals_Int]) 1);