# HG changeset patch
# User paulson
# Date 964002512 -7200
# Node ID e6b96d953965b43bf38744670d29fcbc8e116c3b
# Parent  17c707841ad34ced7384d977ea56f07f7896e094
renamed // to / (which is what we want anyway) to avoid clash with the new
use of // for quotienting

diff -r 17c707841ad3 -r e6b96d953965 src/HOL/Algebra/abstract/Ring.ML
--- a/src/HOL/Algebra/abstract/Ring.ML	Wed Jul 19 10:59:59 2000 +0200
+++ b/src/HOL/Algebra/abstract/Ring.ML	Wed Jul 19 12:28:32 2000 +0200
@@ -4,8 +4,6 @@
     Author: Clemens Ballarin, started 9 December 1996
 *)
 
-open Ring;
-
 Blast.overloaded ("Divides.op dvd", domain_type);
 
 section "Rings";
@@ -21,11 +19,15 @@
 
 val a_ac = [a_assoc, a_comm, a_lcomm];
 
-qed_goal "r_zero" Ring.thy "!!a::'a::ring. a + <0> = a"
-  (fn _ => [rtac (a_comm RS trans) 1, rtac l_zero 1]);
+Goal "!!a::'a::ring. a + <0> = a";
+by (rtac (a_comm RS trans) 1);
+by (rtac l_zero 1);
+qed "r_zero";
 
-qed_goal "r_neg" Ring.thy "!!a::'a::ring. a + (-a) = <0>"
-  (fn _ => [rtac (a_comm RS trans) 1, rtac l_neg 1]);
+Goal "!!a::'a::ring. a + (-a) = <0>";
+by (rtac (a_comm RS trans) 1);
+by (rtac l_neg 1);
+qed "r_neg";
 
 Goal "!! a::'a::ring. a + b = a + c ==> b = c";
 by (rtac box_equals 1);
@@ -74,8 +76,10 @@
 
 val m_ac = [m_assoc, m_comm, m_lcomm];
 
-qed_goal "r_one" Ring.thy "!!a::'a::ring. a * <1> = a"
-  (fn _ => [rtac (m_comm RS trans) 1, rtac l_one 1]);
+Goal "!!a::'a::ring. a * <1> = a";
+by (rtac (m_comm RS trans) 1);
+by (rtac l_one 1);
+qed "r_one";
 
 (* distributive and derived *)
 
@@ -96,8 +100,10 @@
 by (simp_tac (simpset() addsimps [r_zero]) 1);
 qed "l_null";
 
-qed_goal "r_null" Ring.thy "!!a::'a::ring. a * <0> = <0>"
-  (fn _ => [rtac (m_comm RS trans) 1, rtac l_null 1]);
+Goal "!!a::'a::ring. a * <0> = <0>";
+by (rtac (m_comm RS trans) 1);
+by (rtac l_null 1);
+qed "r_null";
 
 Goal "!!a::'a::ring. (-a) * b = - (a * b)";
 by (rtac a_lcancel 1);
@@ -117,12 +123,14 @@
 
 (* one and zero are distinct *)
 
-qed_goal "zero_not_one" Ring.thy "<0> ~= (<1>::'a::ring)"
-  (fn _ => [rtac not_sym 1, rtac one_not_zero 1]);
+Goal "<0> ~= (<1>::'a::ring)";
+by (rtac not_sym 1);
+by (rtac one_not_zero 1);
+qed "zero_not_one";
 
 Addsimps [l_zero, r_zero, l_neg, r_neg, minus_minus, minus0, 
-  l_one, r_one, l_null, r_null,
-  one_not_zero, zero_not_one];
+	  l_one, r_one, l_null, r_null,
+	  one_not_zero, zero_not_one];
 
 (* further rules *)
 
@@ -293,20 +301,17 @@
 
 section "Integral domains";
 
-Goal
-  "!! a. [| a * b = <0>; a ~= <0> |] ==> (b::'a::domain) = <0>";
+Goal "[| a * b = <0>; a ~= <0> |] ==> (b::'a::domain) = <0>";
 by (dtac integral 1);
 by (Fast_tac 1);
 qed "r_integral";
 
-Goal
-  "!! a. [| a * b = <0>; b ~= <0> |] ==> (a::'a::domain) = <0>";
+Goal "[| a * b = <0>; b ~= <0> |] ==> (a::'a::domain) = <0>";
 by (dtac integral 1);
 by (Fast_tac 1);
 qed "l_integral";
 
-Goal
-  "!! a::'a::domain. [| a ~= <0>; b ~= <0> |] ==> a * b ~= <0>";
+Goal "!! a::'a::domain. [| a ~= <0>; b ~= <0> |] ==> a * b ~= <0>";
 by (etac contrapos 1);
 by (rtac l_integral 1);
 by (assume_tac 1);
@@ -389,6 +394,3 @@
 Goalw [prime_def, irred_def] "!! a::'a::field. irred a ==> prime a";
 by (blast_tac (claset() addIs [field_ax]) 1);
 qed "field_fact_prime";
-
-
-
diff -r 17c707841ad3 -r e6b96d953965 src/HOL/Algebra/abstract/Ring.thy
--- a/src/HOL/Algebra/abstract/Ring.thy	Wed Jul 19 10:59:59 2000 +0200
+++ b/src/HOL/Algebra/abstract/Ring.thy	Wed Jul 19 12:28:32 2000 +0200
@@ -24,11 +24,11 @@
 
   (* Fields *)
   inverse	:: 'a::ringS => 'a
-  "'/'/"	:: ['a, 'a] => 'a::ringS		(infixl 70)
+  "'/"		:: ['a, 'a] => 'a::ringS		(infixl 70)
 
 translations
   "a -- b" 	== "a + (-b)"
-  "a // b"	== "a * inverse b"
+  "a / b"	== "a * inverse b"
 
 (* Class ring and ring axioms *)