src/HOL/UNITY/Token.ML

--- a/src/HOL/UNITY/Token.ML	Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/UNITY/Token.ML	Mon Jun 22 17:26:46 1998 +0200
@@ -16,11 +16,11 @@
 
 AddIffs [N_positive, skip];
 
-goalw thy [HasTok_def] "!!i. [| s: HasTok i; s: HasTok j |] ==> i=j";
+Goalw [HasTok_def] "!!i. [| s: HasTok i; s: HasTok j |] ==> i=j";
 by Auto_tac;
 qed "HasToK_partition";
 
-goalw thy Token_defs "!!s. s : WellTyped ==> (s ~: E i) = (s : H i | s : T i)";
+Goalw Token_defs "!!s. s : WellTyped ==> (s ~: E i) = (s : H i | s : T i)";
 by (Simp_tac 1);
 by (exhaust_tac "s (Suc i)" 1);
 by Auto_tac;
@@ -32,7 +32,7 @@
     we'd not have to mention WellTyped in the statement of this theorem.
 **)
 
-goalw thy [stable_def]
+Goalw [stable_def]
     "stable Acts (WellTyped Int {s. s : E i --> s : HasTok i})";
 by (rtac (stable_WT RS stable_constrains_Int) 1);
 by (cut_facts_tac [TR2,TR4,TR5] 1);
@@ -44,7 +44,7 @@
 qed "token_stable";
 
 (*This proof is in the "massaging" style and is much faster! *)
-goalw thy [stable_def]
+Goalw [stable_def]
     "stable Acts (WellTyped Int (Compl(E i) Un (HasTok i)))";
 by (rtac (stable_WT RS stable_constrains_Int) 1);
 by (rtac constrains_weaken 1);
@@ -56,17 +56,17 @@
 
 (*** Progress under weak fairness ***)
 
-goalw thy [nodeOrder_def] "wf(nodeOrder j)";
+Goalw [nodeOrder_def] "wf(nodeOrder j)";
 by (rtac (wf_less_than RS wf_inv_image RS wf_subset) 1);
 by (Blast_tac 1);
 qed"wf_nodeOrder";
 
-    goal thy "!!m. [| m<n; Suc m ~= n |] ==> Suc(m) < n";
+Goal "!!m. [| m<n; Suc m ~= n |] ==> Suc(m) < n";
     by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1);
     by (blast_tac (claset() addEs [less_asym, less_SucE]) 1);
     qed "Suc_lessI";
 
-goalw thy [nodeOrder_def, next_def, inv_image_def]
+Goalw [nodeOrder_def, next_def, inv_image_def]
     "!!x. [| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)";
 by (auto_tac (claset(),
 	      simpset() addsimps [Suc_lessI, mod_Suc, mod_less, mod_geq]));
@@ -99,7 +99,7 @@
 
 (*From "A Logic for Concurrent Programming", but not used in Chapter 4.
   Note the use of case_tac.  Reasoning about leadsTo takes practice!*)
-goal thy
+Goal
  "!!i. [| i<N; j<N |] ==> \
 \      leadsTo Acts (HasTok i) ({s. (Token s, i) : nodeOrder j} Un HasTok j)";
 by (case_tac "i=j" 1);
@@ -111,7 +111,7 @@
 
 
 (*Chapter 4 variant, the one actually used below.*)
-goal thy
+Goal
  "!!i. [| i<N; j<N; i~=j |] ==> \
 \      leadsTo Acts (HasTok i) {s. (Token s, i) : nodeOrder j}";
 by (rtac (TR7 RS leadsTo_weaken_R) 1);
@@ -119,14 +119,14 @@
 by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1);
 qed "TR7_aux";
 
-goal thy "({s. Token s < N} Int Token -`` {m}) = \
+Goal "({s. Token s < N} Int Token -`` {m}) = \
 \         (if m<N then Token -`` {m} else {})";
 by Auto_tac;
 val Token_lemma = result();
 
 
 (*Misra's TR9: the token reaches an arbitrary node*)
-goal thy
+Goal
  "!!i. j<N ==> leadsTo Acts {s. Token s < N} (HasTok j)";
 by (rtac leadsTo_weaken_R 1);
 by (res_inst_tac [("I", "Compl{j}"), ("f", "Token"), ("B", "{}")]
@@ -141,7 +141,7 @@
 qed "leadsTo_j";
 
 (*Misra's TR8: a hungry process eventually eats*)
-goal thy "!!i. j<N ==> leadsTo Acts ({s. Token s < N} Int H j) (E j)";
+Goal "!!i. j<N ==> leadsTo Acts ({s. Token s < N} Int H j) (E j)";
 by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1);
 by (rtac TR6 2);
 by (rtac leadsTo_weaken_R 1);