src/HOL/Integ/Ring.ML

--- a/src/HOL/Integ/Ring.ML	Mon Jun 22 17:13:09 1998 +0200
+++ b/src/HOL/Integ/Ring.ML	Mon Jun 22 17:26:46 1998 +0200
@@ -7,7 +7,7 @@
 and defines cring_simpl, a simplification tactic for commutative rings.
 *)
 
-goal Ring.thy "!!x::'a::cring. x*(y*z)=y*(x*z)";
+Goal "!!x::'a::cring. x*(y*z)=y*(x*z)";
 by (rtac trans 1);
 by (rtac times_commute 1);
 by (rtac trans 1);
@@ -17,7 +17,7 @@
 
 val times_cong = read_instantiate [("f1","op *")] (arg_cong RS cong);
 
-goal Ring.thy "!!x::'a::ring. zero*x = zero";
+Goal "!!x::'a::ring. zero*x = zero";
 by (rtac trans 1);
  by (rtac right_inv 2);
 by (rtac trans 1);
@@ -37,7 +37,7 @@
 by (rtac (zeroR RS sym) 1);
 qed "mult_zeroL";
 
-goal Ring.thy "!!x::'a::ring. x*zero = zero";
+Goal "!!x::'a::ring. x*zero = zero";
 by (rtac trans 1);
  by (rtac right_inv 2);
 by (rtac trans 1);
@@ -57,7 +57,7 @@
 by (rtac (zeroR RS sym) 1);
 qed "mult_zeroR";
 
-goal Ring.thy "!!x::'a::ring. (zero-x)*y = zero-(x*y)";
+Goal "!!x::'a::ring. (zero-x)*y = zero-(x*y)";
 by (rtac trans 1);
  by (rtac zeroL 2);
 by (rtac trans 1);
@@ -83,7 +83,7 @@
 by (rtac (zeroR RS sym) 1);
 qed "mult_invL";
 
-goal Ring.thy "!!x::'a::ring. x*(zero-y) = zero-(x*y)";
+Goal "!!x::'a::ring. x*(zero-y) = zero-(x*y)";
 by (rtac trans 1);
  by (rtac zeroL 2);
 by (rtac trans 1);
@@ -109,12 +109,12 @@
 by (rtac (zeroR RS sym) 1);
 qed "mult_invR";
 
-goal Ring.thy "x*(y-z) = (x*y - x*z::'a::ring)";
+Goal "x*(y-z) = (x*y - x*z::'a::ring)";
 by (mk_group1_tac 1);
 by (simp_tac (HOL_basic_ss addsimps [distribL,mult_invR]) 1);
 qed "minus_distribL";
 
-goal Ring.thy "(x-y)*z = (x*z - y*z::'a::ring)";
+Goal "(x-y)*z = (x*z - y*z::'a::ring)";
 by (mk_group1_tac 1);
 by (simp_tac (HOL_basic_ss addsimps [distribR,mult_invL]) 1);
 qed "minus_distribR";