--- a/src/ZF/Resid/SubUnion.thy Thu Jun 22 12:58:39 1995 +0200
+++ b/src/ZF/Resid/SubUnion.thy Thu Jun 22 17:13:05 1995 +0200
@@ -23,10 +23,10 @@
intrs
Sub_Var "n:nat ==> Var(n)<== Var(n)"
Sub_Fun "[|u<== v|]==> Fun(u)<== Fun(v)"
- Sub_App1 "[|u1<== v1; u2<== v2; b:bool|]==> \
-\ App(0,u1,u2)<== App(b,v1,v2)"
- Sub_App2 "[|u1<== v1; u2<== v2|]==> \
-\ App(1,u1,u2)<== App(1,v1,v2)"
+ Sub_App1 "[|u1<== v1; u2<== v2; b:bool|]==>
+ App(0,u1,u2)<== App(b,v1,v2)"
+ Sub_App2 "[|u1<== v1; u2<== v2|]==>
+ App(1,u1,u2)<== App(1,v1,v2)"
type_intrs "redexes.intrs@bool_typechecks"
inductive
@@ -34,8 +34,8 @@
intrs
Comp_Var "n:nat ==> Var(n) ~ Var(n)"
Comp_Fun "[|u ~ v|]==> Fun(u) ~ Fun(v)"
- Comp_App "[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==> \
-\ App(b1,u1,u2) ~ App(b2,v1,v2)"
+ Comp_App "[|u1 ~ v1; u2 ~ v2; b1:bool; b2:bool|]==>
+ App(b1,u1,u2) ~ App(b2,v1,v2)"
type_intrs "redexes.intrs@bool_typechecks"
inductive
@@ -43,17 +43,17 @@
intrs
Reg_Var "n:nat ==> regular(Var(n))"
Reg_Fun "[|regular(u)|]==> regular(Fun(u))"
- Reg_App1 "[|regular(Fun(u)); regular(v) \
-\ |]==>regular(App(1,Fun(u),v))"
- Reg_App2 "[|regular(u); regular(v) \
-\ |]==>regular(App(0,u,v))"
+ Reg_App1 "[|regular(Fun(u)); regular(v)
+ |]==>regular(App(1,Fun(u),v))"
+ Reg_App2 "[|regular(u); regular(v)
+ |]==>regular(App(0,u,v))"
type_intrs "redexes.intrs@bool_typechecks"
defs
- union_def "u un v == redex_rec(u, \
-\ %i.lam t:redexes.redexes_case(%j.Var(i), %x.0, %b x y.0, t), \
-\ %x m.lam t:redexes.redexes_case(%j.0, %y.Fun(m`y), %b y z.0, t), \
-\%b x y m p.lam t:redexes.redexes_case(%j.0, %y.0, \
-\ %c z u. App(b or c, m`z, p`u), t))`v"
+ union_def "u un v == redex_rec(u,
+ %i.lam t:redexes.redexes_case(%j.Var(i), %x.0, %b x y.0, t),
+ %x m.lam t:redexes.redexes_case(%j.0, %y.Fun(m`y), %b y z.0, t),
+%b x y m p.lam t:redexes.redexes_case(%j.0, %y.0,
+ %c z u. App(b or c, m`z, p`u), t))`v"
end