diff -r 295bb029170c -r a356fb49e69e src/HOL/Integ/IntDef.ML
--- a/src/HOL/Integ/IntDef.ML	Tue Sep 29 12:07:31 1998 +0200
+++ b/src/HOL/Integ/IntDef.ML	Tue Sep 29 15:57:42 1998 +0200
@@ -137,7 +137,7 @@
 by (Asm_full_simp_tac 1);
 qed "inj_zminus";
 
-Goalw [int_def] "- ($# 0) = $# 0";
+Goalw [int_def] "- (int 0) = int 0";
 by (simp_tac (simpset() addsimps [zminus]) 1);
 qed "zminus_nat0";
 
@@ -147,12 +147,12 @@
 (**** neg: the test for negative integers ****)
 
 
-Goalw [neg_def, int_def] "~ neg($# n)";
+Goalw [neg_def, int_def] "~ neg(int n)";
 by (Simp_tac 1);
 by Safe_tac;
 qed "not_neg_nat";
 
-Goalw [neg_def, int_def] "neg(- $# Suc(n))";
+Goalw [neg_def, int_def] "neg(- (int (Suc n)))";
 by (simp_tac (simpset() addsimps [zminus]) 1);
 qed "neg_zminus_nat";
 
@@ -214,30 +214,30 @@
 (*Integer addition is an AC operator*)
 val zadd_ac = [zadd_assoc,zadd_commute,zadd_left_commute];
 
-Goalw [int_def] "($#m) + ($#n) = $# (m + n)";
+Goalw [int_def] "(int m) + (int n) = int (m + n)";
 by (simp_tac (simpset() addsimps [zadd]) 1);
-qed "add_nat";
+qed "zadd_int";
 
-Goal "$# (Suc m) = $# 1 + ($# m)";
-by (simp_tac (simpset() addsimps [add_nat]) 1);
+Goal "int (Suc m) = int 1 + (int m)";
+by (simp_tac (simpset() addsimps [zadd_int]) 1);
 qed "int_Suc";
 
-Goalw [int_def] "$# 0 + z = z";
+Goalw [int_def] "int 0 + z = z";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps [zadd]) 1);
 qed "zadd_nat0";
 
-Goal "z + $# 0 = z";
+Goal "z + int 0 = z";
 by (rtac (zadd_commute RS trans) 1);
 by (rtac zadd_nat0 1);
 qed "zadd_nat0_right";
 
-Goalw [int_def] "z + (- z) = $# 0";
+Goalw [int_def] "z + (- z) = int 0";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1);
 qed "zadd_zminus_inverse_nat";
 
-Goal "(- z) + z = $# 0";
+Goal "(- z) + z = int 0";
 by (rtac (zadd_commute RS trans) 1);
 by (rtac zadd_zminus_inverse_nat 1);
 qed "zadd_zminus_inverse_nat2";
@@ -246,15 +246,25 @@
 	  zadd_zminus_inverse_nat, zadd_zminus_inverse_nat2];
 
 Goal "z + (- z + w) = (w::int)";
-by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
+by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
 qed "zadd_zminus_cancel";
 
 Goal "(-z) + (z + w) = (w::int)";
-by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
+by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
 qed "zminus_zadd_cancel";
 
 Addsimps [zadd_zminus_cancel, zminus_zadd_cancel];
 
+Goal "int 0 - x = -x";
+by (simp_tac (simpset() addsimps [zdiff_def]) 1);
+qed "zdiff_nat0";
+
+Goal "x - int 0 = x";
+by (simp_tac (simpset() addsimps [zdiff_def]) 1);
+qed "zdiff_nat0_right";
+
+Addsimps [zdiff_nat0, zdiff_nat0_right];
+
 
 (** Lemmas **)
 
@@ -362,21 +372,21 @@
 by (simp_tac (simpset() addsimps [zmult_commute',zadd_zmult_distrib]) 1);
 qed "zadd_zmult_distrib2";
 
-Goalw [int_def] "$# 0 * z = $# 0";
+Goalw [int_def] "int 0 * z = int 0";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps [zmult]) 1);
 qed "zmult_nat0";
 
-Goalw [int_def] "$# 1 * z = z";
+Goalw [int_def] "int 1 * z = z";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (asm_simp_tac (simpset() addsimps [zmult]) 1);
 qed "zmult_nat1";
 
-Goal "z * $# 0 = $# 0";
+Goal "z * int 0 = int 0";
 by (rtac ([zmult_commute, zmult_nat0] MRS trans) 1);
 qed "zmult_nat0_right";
 
-Goal "z * $# 1 = z";
+Goal "z * int 1 = z";
 by (rtac ([zmult_commute, zmult_nat1] MRS trans) 1);
 qed "zmult_nat1_right";
 
@@ -394,7 +404,7 @@
 
 (*This lemma allows direct proofs of other <-properties*)
 Goalw [zless_def, neg_def, zdiff_def, int_def] 
-    "(w < z) = (EX n. z = w + $#(Suc n))";
+    "(w < z) = (EX n. z = w + int(Suc n))";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
 by (Clarify_tac 1);
@@ -404,16 +414,16 @@
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps add_ac)));
 qed "zless_iff_Suc_zadd";
 
-Goal "z < z + $# (Suc n)";
+Goal "z < z + int (Suc n)";
 by (auto_tac (claset(),
 	      simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, 
-				  add_nat]));
+				  zadd_int]));
 qed "zless_zadd_Suc";
 
 Goal "[| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
 by (auto_tac (claset(),
 	      simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, 
-				  add_nat]));
+				  zadd_int]));
 qed "zless_trans";
 
 Goal "!!w::int. z<w ==> ~w<z";
@@ -463,24 +473,24 @@
 (*** eliminates ~= in premises ***)
 bind_thm("int_neqE", int_neq_iff RS iffD1 RS disjE);
 
-Goal "($# m = $# n) = (m = n)"; 
+Goal "(int m = int n) = (m = n)"; 
 by (fast_tac (claset() addSEs [inj_nat RS injD]) 1); 
 qed "int_int_eq"; 
 AddIffs [int_int_eq]; 
 
-Goal "($#m < $#n) = (m<n)";
+Goal "(int m < int n) = (m<n)";
 by (simp_tac (simpset() addsimps [less_iff_Suc_add, zless_iff_Suc_zadd, 
-				  add_nat]) 1);
-qed "zless_eq_less";
-Addsimps [zless_eq_less];
+				  zadd_int]) 1);
+qed "zless_int";
+Addsimps [zless_int];
 
 
 (*** Properties of <= ***)
 
-Goalw [zle_def, le_def] "($#m <= $#n) = (m<=n)";
+Goalw [zle_def, le_def] "(int m <= int n) = (m<=n)";
 by (Simp_tac 1);
-qed "zle_eq_le";
-Addsimps [zle_eq_le];
+qed "zle_int";
+Addsimps [zle_int];
 
 Goalw [zle_def] "~(w<z) ==> z<=(w::int)";
 by (assume_tac 1);
@@ -633,10 +643,9 @@
 Addsimps [zadd_right_cancel];
 
 
-Goal "(w < z + $# 1) = (w<z | w=z)";
+Goal "(w < z + int 1) = (w<z | w=z)";
 by (auto_tac (claset(),
-	      simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, 
-				  add_nat]));
+	      simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, zadd_int]));
 by (cut_inst_tac [("m","n")] int_Suc 1);
 by (exhaust_tac "n" 1);
 by Auto_tac;
@@ -645,8 +654,9 @@
 qed "zless_add_nat1_eq";
 
 
-Goal "(w + $# 1 <= z) = (w<z)";
+Goal "(w + int 1 <= z) = (w<z)";
 by (simp_tac (simpset() addsimps [zle_def, zless_add_nat1_eq]) 1);
 by (auto_tac (claset() addIs [zle_anti_sym] addEs [zless_asym],
 	      simpset() addsimps [symmetric zle_def]));
 qed "add_nat1_zle_eq";
+