src/HOL/Univ.thy
changeset 5978 fa2c2dd74f8c
parent 5191 8ceaa19f7717
child 7014 11ee650edcd2
     1.1 --- a/src/HOL/Univ.thy	Thu Nov 26 17:40:10 1998 +0100
     1.2 +++ b/src/HOL/Univ.thy	Fri Nov 27 10:40:29 1998 +0100
     1.3 @@ -42,7 +42,6 @@
     1.4    Split  :: [['a item, 'a item]=>'b, 'a item] => 'b
     1.5    Case   :: [['a item]=>'b, ['a item]=>'b, 'a item] => 'b
     1.6  
     1.7 -  diag   :: "'a set => ('a * 'a)set"
     1.8    "<**>" :: "[('a item * 'a item)set, ('a item * 'a item)set] 
     1.9             => ('a item * 'a item)set" (infixr 80)
    1.10    "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] 
    1.11 @@ -88,13 +87,11 @@
    1.12                                | (? y . M = In1(y) & u = d(y))"
    1.13  
    1.14  
    1.15 -  (** diagonal sets and equality for the "universe" **)
    1.16 -
    1.17 -  diag_def   "diag(A) == UN x:A. {(x,x)}"
    1.18 +  (** equality for the "universe" **)
    1.19  
    1.20    dprod_def  "r<**>s == UN (x,x'):r. UN (y,y'):s. {(Scons x y, Scons x' y')}"
    1.21  
    1.22    dsum_def   "r<++>s == (UN (x,x'):r. {(In0(x),In0(x'))}) Un 
    1.23 -                       (UN (y,y'):s. {(In1(y),In1(y'))})"
    1.24 +                        (UN (y,y'):s. {(In1(y),In1(y'))})"
    1.25  
    1.26  end