# HG changeset patch
# User paulson
# Date 963224254 -7200
# Node ID 85a5355faa9129a7b172f319345b87bf2a1a1b85
# Parent  04f1b522cb1170637ce7cc3f860098463cdf56bf
removal of (harmless) circular definitions

diff -r 04f1b522cb11 -r 85a5355faa91 src/ZF/Resid/Redex.thy
--- a/src/ZF/Resid/Redex.thy	Sun Jul 09 16:01:42 2000 +0200
+++ b/src/ZF/Resid/Redex.thy	Mon Jul 10 12:17:34 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Redex.thy
+(*  Title:      ZF/Resid/Redex.thy
     ID:         $Id$
     Author:     Ole Rasmussen
     Copyright   1995  University of Cambridge
@@ -22,28 +22,29 @@
   union_aux        :: i=>i
   regular          :: i=>o
   
+translations
+  "a<==b"        == "<a,b>:Ssub"
+  "a ~ b"        == "<a,b>:Scomp"
+  "regular(a)"   == "a:Sreg"
+
+
 primrec (*explicit lambda is required because both arguments of "un" vary*)
   "union_aux(Var(n)) =
      (lam t:redexes. redexes_case(%j. Var(n), %x. 0, %b x y.0, t))"
 
   "union_aux(Fun(u)) =
-     (lam t:redexes. redexes_case(%j. 0, %y. Fun(u un y),
+     (lam t:redexes. redexes_case(%j. 0, %y. Fun(union_aux(u)`y),
 	 			  %b y z. 0, t))"
 
   "union_aux(App(b,f,a)) =
      (lam t:redexes.
         redexes_case(%j. 0, %y. 0,
-		     %c z u. App(b or c, f un z, a un u), t))"
+		     %c z u. App(b or c, union_aux(f)`z, union_aux(a)`u), t))"
 
 defs
   union_def  "u un v == union_aux(u)`v"
 
 
-translations
-  "a<==b"        == "<a,b>:Ssub"
-  "a ~ b"        == "<a,b>:Scomp"
-  "regular(a)"   == "a:Sreg"
-
 inductive
   domains       "Ssub" <= "redexes*redexes"
   intrs
diff -r 04f1b522cb11 -r 85a5355faa91 src/ZF/Resid/Substitution.thy
--- a/src/ZF/Resid/Substitution.thy	Sun Jul 09 16:01:42 2000 +0200
+++ b/src/ZF/Resid/Substitution.thy	Mon Jul 10 12:17:34 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      Substitution.thy
+(*  Title:      ZF/Resid/Substitution.thy
     ID:         $Id$
     Author:     Ole Rasmussen
     Copyright   1995  University of Cambridge
@@ -42,10 +42,10 @@
      (lam r:redexes. lam k:nat. if k<i then Var(i #- 1) 
 				else if k=i then r else Var(i))"
   "subst_aux(Fun(t)) =
-     (lam r:redexes. lam k:nat. Fun(subst_rec(lift(r), t, succ(k))))"
+     (lam r:redexes. lam k:nat. Fun(subst_aux(t) ` lift(r) ` succ(k)))"
 
   "subst_aux(App(b,f,a)) = 
-     (lam r:redexes. lam k:nat. App(b, subst_rec(r,f,k), subst_rec(r,a,k)))"
+     (lam r:redexes. lam k:nat. App(b, subst_aux(f)`r`k, subst_aux(a)`r`k))"
 
 end