--- a/Univ.thy Thu Feb 24 14:45:57 1994 +0100
+++ b/Univ.thy Wed Mar 02 12:26:55 1994 +0100
@@ -29,7 +29,7 @@
Atom :: "('a+nat) => 'a node set"
Leaf :: "'a => 'a node set"
Numb :: "nat => 'a node set"
- "." :: "['a node set, 'a node set]=> 'a node set" (infixr 60)
+ "$" :: "['a node set, 'a node set]=> 'a node set" (infixr 60)
In0,In1 :: "'a node set => 'a node set"
ntrunc :: "[nat, 'a node set] => 'a node set"
@@ -67,26 +67,26 @@
(*S-expression constructors*)
Atom_def "Atom == (%x. {Abs_Node(<%k.0, x>)})"
- Scons_def "M.N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)"
+ Scons_def "M$N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)"
(*Leaf nodes, with arbitrary or nat labels*)
Leaf_def "Leaf == Atom o Inl"
Numb_def "Numb == Atom o Inr"
(*Injections of the "disjoint sum"*)
- In0_def "In0(M) == Numb(0) . M"
- In1_def "In1(M) == Numb(Suc(0)) . M"
+ In0_def "In0(M) == Numb(0) $ M"
+ In1_def "In1(M) == Numb(Suc(0)) $ M"
(*the set of nodes with depth less than k*)
ndepth_def "ndepth(n) == split(Rep_Node(n), %f x. LEAST k. f(k)=0)"
ntrunc_def "ntrunc(k,N) == {n. n:N & ndepth(n)<k}"
(*products and sums for the "universe"*)
- uprod_def "A<*>B == UN x:A. UN y:B. { (x.y) }"
+ uprod_def "A<*>B == UN x:A. UN y:B. { (x$y) }"
usum_def "A<+>B == In0``A Un In1``B"
(*the corresponding eliminators*)
- Split_def "Split(M,c) == @u. ? x y. M = x.y & u = c(x,y)"
+ Split_def "Split(M,c) == @u. ? x y. M = x$y & u = c(x,y)"
Case_def "Case(M,c,d) == @u. (? x . M = In0(x) & u = c(x)) \
\ | (? y . M = In1(y) & u = d(y))"
@@ -97,7 +97,7 @@
diag_def "diag(A) == UN x:A. {<x,x>}"
dprod_def "r<**>s == UN u:r. UN v:s. \
-\ split(u, %x x'. split(v, %y y'. {<x.y,x'.y'>}))"
+\ split(u, %x x'. split(v, %y y'. {<x$y,x'$y'>}))"
dsum_def "r<++>s == (UN u:r. split(u, %x x'. {<In0(x),In0(x')>})) Un \
\ (UN v:s. split(v, %y y'. {<In1(y),In1(y')>}))"