src/HOL/Lambda/Commutation.ML

--- a/src/HOL/Lambda/Commutation.ML	Thu Jul 02 17:58:12 1998 +0200
+++ b/src/HOL/Lambda/Commutation.ML	Fri Jul 03 10:36:47 1998 +0200
@@ -10,22 +10,22 @@
 
 (*** square ***)
 
-Goalw [square_def] "!!R. square R S T U ==> square S R U T";
+Goalw [square_def] "square R S T U ==> square S R U T";
 by (Blast_tac 1);
 qed "square_sym";
 
 Goalw [square_def]
-  "!!R. [| square R S T U; T <= T' |] ==> square R S T' U";
+  "[| square R S T U; T <= T' |] ==> square R S T' U";
 by (Blast_tac 1);
 qed "square_subset";
 
 Goalw [square_def]
-  "!!R. [| square R S T (R^=); S <= T |] ==> square (R^=) S T (R^=)";
+  "[| square R S T (R^=); S <= T |] ==> square (R^=) S T (R^=)";
 by (Blast_tac 1);
 qed "square_reflcl";
 
 Goalw [square_def]
-  "!!R. square R S S T ==> square (R^*) S S (T^*)";
+  "square R S S T ==> square (R^*) S S (T^*)";
 by (strip_tac 1);
 by (etac rtrancl_induct 1);
 by (Blast_tac 1);
@@ -33,7 +33,7 @@
 qed "square_rtrancl";
 
 Goalw [commute_def]
- "!!R. square R S (S^*) (R^=) ==> commute (R^*) (S^*)";
+ "square R S (S^*) (R^=) ==> commute (R^*) (S^*)";
 by (fast_tac (claset() addDs [square_reflcl,square_sym RS square_rtrancl]
                        addEs [r_into_rtrancl]
                        addss simpset()) 1);
@@ -41,45 +41,43 @@
 
 (*** commute ***)
 
-Goalw [commute_def] "!!R. commute R S ==> commute S R";
+Goalw [commute_def] "commute R S ==> commute S R";
 by (blast_tac (claset() addIs [square_sym]) 1);
 qed "commute_sym";
 
-Goalw [commute_def] "!!R. commute R S ==> commute (R^*) (S^*)";
+Goalw [commute_def] "commute R S ==> commute (R^*) (S^*)";
 by (blast_tac (claset() addIs [square_rtrancl,square_sym]) 1);
 qed "commute_rtrancl";
 
 Goalw [commute_def,square_def]
-  "!!R. [| commute R T; commute S T |] ==> commute (R Un S) T";
+  "[| commute R T; commute S T |] ==> commute (R Un S) T";
 by (Blast_tac 1);
 qed "commute_Un";
 
 (*** diamond, confluence and union ***)
 
 Goalw [diamond_def]
-  "!!R. [| diamond R; diamond S; commute R S |] ==> diamond (R Un S)";
+  "[| diamond R; diamond S; commute R S |] ==> diamond (R Un S)";
 by (REPEAT(ares_tac [commute_Un,commute_sym] 1));
 qed "diamond_Un";
 
-Goalw [diamond_def] "!!R. diamond R ==> confluent (R)";
+Goalw [diamond_def] "diamond R ==> confluent (R)";
 by (etac commute_rtrancl 1);
 qed "diamond_confluent";
 
 Goalw [diamond_def]
-  "!!R. square R R (R^=) (R^=) ==> confluent 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
- "!!R. [| confluent R; confluent S; commute (R^*) (S^*) |] \
-\      ==> confluent(R Un S)";
+ "[| 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
-  "!!R.[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)";
+Goal "[| diamond(R); T <= R; R <= T^* |] ==> confluent(T)";
 by (fast_tac (claset() addIs [diamond_confluent] addDs [rtrancl_subset RS sym] 
 		       addss simpset()) 1);
 qed "diamond_to_confluence";