src/HOL/Univ.thy
changeset 3947 eb707467f8c5
parent 1562 e98c7f6165c9
child 5191 8ceaa19f7717
     1.1 --- a/src/HOL/Univ.thy	Mon Oct 20 11:22:29 1997 +0200
     1.2 +++ b/src/HOL/Univ.thy	Mon Oct 20 11:25:39 1997 +0200
     1.3 @@ -13,6 +13,8 @@
     1.4  
     1.5  (** lists, trees will be sets of nodes **)
     1.6  
     1.7 +global
     1.8 +
     1.9  typedef (Node)
    1.10    'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}"
    1.11  
    1.12 @@ -46,6 +48,9 @@
    1.13    "<++>" :: "[('a item * 'a item)set, ('a item * 'a item)set] 
    1.14             => ('a item * 'a item)set" (infixr 70)
    1.15  
    1.16 +
    1.17 +local
    1.18 +
    1.19  defs
    1.20  
    1.21    Push_Node_def  "Push_Node == (%n x. Abs_Node (apfst (Push n) (Rep_Node x)))"