# HG changeset patch
# User paulson
# Date 906367618 -7200
# Node ID 324e1560a5c9ad3230debc7f7969a09297419805
# Parent  3896c7894a57daf21b4303d1f24786ae8833b8b6
inserted space in #-1 to prevent confusion with an integer constant

diff -r 3896c7894a57 -r 324e1560a5c9 src/ZF/Resid/Substitution.ML
--- a/src/ZF/Resid/Substitution.ML	Mon Sep 21 10:43:54 1998 +0200
+++ b/src/ZF/Resid/Substitution.ML	Mon Sep 21 10:46:58 1998 +0200
@@ -23,14 +23,14 @@
               (Asm_simp_tac 1)]);
 
 goal Arith.thy 
-    "!!i.[|succ(x)<n; n:nat; x:nat|]==> x < n#-1 ";
+    "!!i.[|succ(x)<n; n:nat; x:nat|]==> x < n #- 1 ";
 by (rtac succ_leE 1);
 by (forward_tac [nat_into_Ord RS le_refl RS lt_trans] 1 THEN assume_tac 1);
 by (asm_simp_tac (simpset() addsimps [succ_pred]) 1);
 qed "lt_pred";
 
 goal Arith.thy 
-    "!!i.[|n < succ(x); p<n; p:nat; n:nat; x:nat|]==> n#-1 < x ";
+    "!!i.[|n < succ(x); p<n; p:nat; n:nat; x:nat|]==> n #- 1 < x ";
 by (rtac succ_leE 1);
 by (asm_simp_tac (simpset() addsimps [succ_pred]) 1);
 qed "gt_pred";
@@ -75,7 +75,7 @@
 
 Goalw [subst_rec_def] 
     "[|i:nat; k:nat; u:redexes|]==>  \
-\        subst_rec(u,Var(i),k) = if(k<i,Var(i#-1),if(k=i,u,Var(i)))";
+\        subst_rec(u,Var(i),k) = if(k<i,Var(i #- 1),if(k=i,u,Var(i)))";
 by (asm_full_simp_tac (simpset() addsimps [gt_not_eq,leI]) 1);
 qed "subst_Var";
 
@@ -86,7 +86,7 @@
 
 Goalw [subst_rec_def] 
     "[|n:nat; u:redexes; p:nat; p<n|]==>  \
-\        subst_rec(u,Var(n),p) = Var(n#-1)";
+\        subst_rec(u,Var(n),p) = Var(n #- 1)";
 by (asm_full_simp_tac (simpset()) 1);
 qed "subst_gt";
 
diff -r 3896c7894a57 -r 324e1560a5c9 src/ZF/Resid/Substitution.thy
--- a/src/ZF/Resid/Substitution.thy	Mon Sep 21 10:43:54 1998 +0200
+++ b/src/ZF/Resid/Substitution.thy	Mon Sep 21 10:46:58 1998 +0200
@@ -33,7 +33,7 @@
   subst_rec_def "subst_rec(u,t,kg) ==   
                      redex_rec(t,   
                        %i.(lam r:redexes. lam k:nat.   
-                              if(k<i,Var(i#-1),   
+                              if(k<i,Var(i #- 1),   
                                 if(k=i,r,Var(i)))),   
                        %x m.(lam r:redexes. lam k:nat.   
                              Fun(m`(lift(r))`(succ(k)))),   
diff -r 3896c7894a57 -r 324e1560a5c9 src/ZF/ex/Limit.ML
--- a/src/ZF/ex/Limit.ML	Mon Sep 21 10:43:54 1998 +0200
+++ b/src/ZF/ex/Limit.ML	Mon Sep 21 10:46:58 1998 +0200
@@ -1465,7 +1465,7 @@
       [asm_simp_tac (simpset() addsimps[add_succ_right,add_0_right]) 1]);
 
 Goal  (* succ_sub1 *)
-    "x:nat ==> 0 < x --> succ(x#-1)=x";
+    "x:nat ==> 0 < x --> succ(x #- 1)=x";
 by (res_inst_tac[("n","x")]nat_induct 1);
 by (assume_tac 1);
 by (Fast_tac 1);