src/HOL/Univ.thy
changeset 972 e61b058d58d2
parent 923 ff1574a81019
child 1068 e0f2dffab506
     1.1 --- a/src/HOL/Univ.thy	Thu Mar 23 15:39:13 1995 +0100
     1.2 +++ b/src/HOL/Univ.thy	Fri Mar 24 12:30:35 1995 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4  (** lists, trees will be sets of nodes **)
     1.5  
     1.6  subtype (Node)
     1.7 -  'a node = "{p. EX f x k. p = <f::nat=>nat, x::'a+nat> & f(k)=0}"
     1.8 +  'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}"
     1.9  
    1.10  types
    1.11    'a item = "'a node set"
    1.12 @@ -58,13 +58,13 @@
    1.13    Push_Node_def  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"
    1.14  
    1.15    (*crude "lists" of nats -- needed for the constructions*)
    1.16 -  apfst_def  "apfst == (%f. split(%x y. <f(x),y>))"
    1.17 +  apfst_def  "apfst == (%f. split(%x y. (f(x),y)))"
    1.18    Push_def   "Push == (%b h. nat_case (Suc b) h)"
    1.19  
    1.20    (** operations on S-expressions -- sets of nodes **)
    1.21  
    1.22    (*S-expression constructors*)
    1.23 -  Atom_def   "Atom == (%x. {Abs_Node(<%k.0, x>)})"
    1.24 +  Atom_def   "Atom == (%x. {Abs_Node((%k.0, x))})"
    1.25    Scons_def  "M$N == (Push_Node(0) `` M) Un (Push_Node(Suc(0)) `` N)"
    1.26  
    1.27    (*Leaf nodes, with arbitrary or nat labels*)
    1.28 @@ -92,12 +92,12 @@
    1.29  
    1.30    (** diagonal sets and equality for the "universe" **)
    1.31  
    1.32 -  diag_def   "diag(A) == UN x:A. {<x,x>}"
    1.33 +  diag_def   "diag(A) == UN x:A. {(x,x)}"
    1.34  
    1.35    dprod_def  "r<**>s == UN u:r. split (%x x'. \
    1.36 -\                       UN v:s. split (%y y'. {<x$y,x'$y'>}) v) u"
    1.37 +\                       UN v:s. split (%y y'. {(x$y,x'$y')}) v) u"
    1.38  
    1.39 -  dsum_def   "r<++>s == (UN u:r. split (%x x'. {<In0(x),In0(x')>}) u) Un \
    1.40 -\                       (UN v:s. split (%y y'. {<In1(y),In1(y')>}) v)"
    1.41 +  dsum_def   "r<++>s == (UN u:r. split (%x x'. {(In0(x),In0(x'))}) u) Un \
    1.42 +\                       (UN v:s. split (%y y'. {(In1(y),In1(y'))}) v)"
    1.43  
    1.44  end