--- a/src/HOL/Ring_and_Field.thy Wed Jan 28 01:19:34 2004 +0100
+++ b/src/HOL/Ring_and_Field.thy Wed Jan 28 10:41:49 2004 +0100
@@ -1625,8 +1625,12 @@
val divide_inverse = thm"divide_inverse";
val inverse_zero = thm"inverse_zero";
val divide_zero = thm"divide_zero";
+
val add_0 = thm"add_0";
val add_0_right = thm"add_0_right";
+val add_zero_left = thm"add_0";
+val add_zero_right = thm"add_0_right";
+
val add_left_commute = thm"add_left_commute";
val left_minus = thm"left_minus";
val right_minus = thm"right_minus";