Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/Resid/Substitution.thy
changeset 5514 324e1560a5c9
parent 3840 e0baea4d485a
child 6046 2c8a8be36c94 
--- 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)))),
isabelle