diff -r fb28eaa07e01 -r 3ea049f7979d src/HOL/Lambda/Commutation.ML
--- a/src/HOL/Lambda/Commutation.ML	Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/Lambda/Commutation.ML	Mon Jun 22 17:26:46 1998 +0200
@@ -10,21 +10,21 @@
 
 (*** square ***)
 
-goalw Commutation.thy [square_def] "!!R. square R S T U ==> square S R U T";
+Goalw [square_def] "!!R. square R S T U ==> square S R U T";
 by (Blast_tac 1);
 qed "square_sym";
 
-goalw Commutation.thy [square_def]
+Goalw [square_def]
   "!!R. [| square R S T U; T <= T' |] ==> square R S T' U";
 by (Blast_tac 1);
 qed "square_subset";
 
-goalw Commutation.thy [square_def]
+Goalw [square_def]
   "!!R. [| square R S T (R^=); S <= T |] ==> square (R^=) S T (R^=)";
 by (Blast_tac 1);
 qed "square_reflcl";
 
-goalw Commutation.thy [square_def]
+Goalw [square_def]
   "!!R. square R S S T ==> square (R^*) S S (T^*)";
 by (strip_tac 1);
 by (etac rtrancl_induct 1);
@@ -32,7 +32,7 @@
 by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
 qed "square_rtrancl";
 
-goalw Commutation.thy [commute_def]
+Goalw [commute_def]
  "!!R. square R S (S^*) (R^=) ==> commute (R^*) (S^*)";
 by (fast_tac (claset() addDs [square_reflcl,square_sym RS square_rtrancl]
                        addEs [r_into_rtrancl]
@@ -41,44 +41,44 @@
 
 (*** commute ***)
 
-goalw Commutation.thy [commute_def] "!!R. commute R S ==> commute S R";
+Goalw [commute_def] "!!R. commute R S ==> commute S R";
 by (blast_tac (claset() addIs [square_sym]) 1);
 qed "commute_sym";
 
-goalw Commutation.thy [commute_def] "!!R. commute R S ==> commute (R^*) (S^*)";
+Goalw [commute_def] "!!R. commute R S ==> commute (R^*) (S^*)";
 by (blast_tac (claset() addIs [square_rtrancl,square_sym]) 1);
 qed "commute_rtrancl";
 
-goalw Commutation.thy [commute_def,square_def]
+Goalw [commute_def,square_def]
   "!!R. [| commute R T; commute S T |] ==> commute (R Un S) T";
 by (Blast_tac 1);
 qed "commute_Un";
 
 (*** diamond, confluence and union ***)
 
-goalw Commutation.thy [diamond_def]
+Goalw [diamond_def]
   "!!R. [| diamond R; diamond S; commute R S |] ==> diamond (R Un S)";
 by (REPEAT(ares_tac [commute_Un,commute_sym] 1));
 qed "diamond_Un";
 
-goalw Commutation.thy [diamond_def] "!!R. diamond R ==> confluent (R)";
+Goalw [diamond_def] "!!R. diamond R ==> confluent (R)";
 by (etac commute_rtrancl 1);
 qed "diamond_confluent";
 
-goalw Commutation.thy [diamond_def]
+Goalw [diamond_def]
   "!!R. square R R (R^=) (R^=) ==> confluent R";
 by (fast_tac (claset() addIs [square_rtrancl_reflcl_commute, r_into_rtrancl]
                        addEs [square_subset]) 1);
 qed "square_reflcl_confluent";
 
-goal Commutation.thy
+Goal
  "!!R. [| confluent R; confluent S; commute (R^*) (S^*) |] \
 \      ==> confluent(R Un S)";
 by (rtac (rtrancl_Un_rtrancl RS subst) 1);
 by (blast_tac (claset() addDs [diamond_Un] addIs [diamond_confluent]) 1);
 qed "confluent_Un";
 
-goal Commutation.thy
+Goal
   "!!R.[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)";
 by (fast_tac (claset() addIs [diamond_confluent] addDs [rtrancl_subset RS sym] 
 		       addss simpset()) 1);
@@ -86,7 +86,7 @@
 
 (*** Church_Rosser ***)
 
-goalw Commutation.thy [square_def,commute_def,diamond_def,Church_Rosser_def]
+Goalw [square_def,commute_def,diamond_def,Church_Rosser_def]
   "Church_Rosser(R) = confluent(R)";
 by (safe_tac HOL_cs);
  by (blast_tac (HOL_cs addIs