--- a/Univ.thy Fri Apr 14 11:23:33 1995 +0200
+++ b/Univ.thy Wed Jun 21 15:12:40 1995 +0200
@@ -45,10 +45,10 @@
Case :: "[['a item]=>'b, ['a item]=>'b, 'a item] => 'b"
diag :: "'a set => ('a * 'a)set"
- "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set] \
-\ => ('a item * 'a item)set" (infixr 80)
- "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] \
-\ => ('a item * 'a item)set" (infixr 70)
+ "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set]
+ => ('a item * 'a item)set" (infixr 80)
+ "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set]
+ => ('a item * 'a item)set" (infixr 70)
defs
@@ -86,18 +86,18 @@
(*the corresponding eliminators*)
Split_def "Split(c,M) == @u. ? x y. M = x$y & u = c(x,y)"
- Case_def "Case(c,d,M) == @u. (? x . M = In0(x) & u = c(x)) \
-\ | (? y . M = In1(y) & u = d(y))"
+ Case_def "Case(c,d,M) == @u. (? x . M = In0(x) & u = c(x))
+ | (? y . M = In1(y) & u = d(y))"
(** diagonal sets and equality for the "universe" **)
diag_def "diag(A) == UN x:A. {<x,x>}"
- dprod_def "r<**>s == UN u:r. split(%x x'. \
-\ UN v:s. split(%y y'. {<x$y,x'$y'>}, v), u)"
+ dprod_def "r<**>s == UN u:r. split(%x x'.
+ UN v:s. split(%y y'. {<x$y,x'$y'>}, v), u)"
- dsum_def "r<++>s == (UN u:r. split(%x x'. {<In0(x),In0(x')>}, u)) Un \
-\ (UN v:s. split(%y y'. {<In1(y),In1(y')>}, v))"
+ dsum_def "r<++>s == (UN u:r. split(%x x'. {<In0(x),In0(x')>}, u)) Un
+ (UN v:s. split(%y y'. {<In1(y),In1(y')>}, v))"
end