src/HOL/RelPow.ML

--- a/src/HOL/RelPow.ML	Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/RelPow.ML	Mon Jun 22 17:26:46 1998 +0200
@@ -6,28 +6,28 @@
 
 open RelPow;
 
-goal RelPow.thy "!!R:: ('a*'a)set. R^1 = R";
+Goal "!!R:: ('a*'a)set. R^1 = R";
 by (Simp_tac 1);
 qed "rel_pow_1";
 Addsimps [rel_pow_1];
 
-goal RelPow.thy "(x,x) : R^0";
+Goal "(x,x) : R^0";
 by (Simp_tac 1);
 qed "rel_pow_0_I";
 
-goal RelPow.thy "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
+Goal "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
 by (Simp_tac  1);
 by (Blast_tac 1);
 qed "rel_pow_Suc_I";
 
-goal RelPow.thy "!z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)";
+Goal "!z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)";
 by (nat_ind_tac "n" 1);
 by (Simp_tac  1);
 by (Asm_full_simp_tac 1);
 by (Blast_tac 1);
 qed_spec_mp "rel_pow_Suc_I2";
 
-goal RelPow.thy "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P";
+Goal "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P";
 by (Asm_full_simp_tac 1);
 qed "rel_pow_0_E";
 
@@ -51,14 +51,14 @@
 by (REPEAT(ares_tac [p3] 1));
 qed "rel_pow_E";
 
-goal RelPow.thy "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
+Goal "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
 by (nat_ind_tac "n" 1);
 by (blast_tac (claset() addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
 by (blast_tac (claset() addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
 qed_spec_mp "rel_pow_Suc_D2";
 
 
-goal RelPow.thy
+Goal
 "!x y z. (x,y) : R^n & (y,z) : R --> (? w. (x,w) : R & (w,z) : R^n)";
 by (nat_ind_tac "n" 1);
 by (fast_tac (claset() addss (simpset())) 1);
@@ -83,30 +83,30 @@
 by (etac conjunct2 1);
 qed "rel_pow_E2";
 
-goal RelPow.thy "!!p. p:R^* ==> p : (UN n. R^n)";
+Goal "!!p. p:R^* ==> p : (UN n. R^n)";
 by (split_all_tac 1);
 by (etac rtrancl_induct 1);
 by (ALLGOALS (blast_tac (claset() addIs [rel_pow_0_I,rel_pow_Suc_I])));
 qed "rtrancl_imp_UN_rel_pow";
 
-goal RelPow.thy "!y. (x,y):R^n --> (x,y):R^*";
+Goal "!y. (x,y):R^n --> (x,y):R^*";
 by (nat_ind_tac "n" 1);
 by (blast_tac (claset() addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
 by (blast_tac (claset() addEs [rel_pow_Suc_E]
                        addIs [rtrancl_into_rtrancl]) 1);
 val lemma = result() RS spec RS mp;
 
-goal RelPow.thy "!!p. p:R^n ==> p:R^*";
+Goal "!!p. p:R^n ==> p:R^*";
 by (split_all_tac 1);
 by (etac lemma 1);
 qed "rel_pow_imp_rtrancl";
 
-goal RelPow.thy "R^* = (UN n. R^n)";
+Goal "R^* = (UN n. R^n)";
 by (blast_tac (claset() addIs [rtrancl_imp_UN_rel_pow, rel_pow_imp_rtrancl]) 1);
 qed "rtrancl_is_UN_rel_pow";
 
 
-goal RelPow.thy "!!r::('a * 'a)set. Univalent r ==> Univalent (r^n)";
+Goal "!!r::('a * 'a)set. Univalent r ==> Univalent (r^n)";
 by (rtac UnivalentI 1);
 by (induct_tac "n" 1);
  by (Simp_tac 1);