constdefs
authorpaulson
Thu Jan 28 18:10:17 1999 +0100 (1999-01-28)
changeset 6159833b76d0e6dc
parent 6158 981f96a598f5
child 6160 32c0b8f57bb7
constdefs
src/ZF/ex/Term.thy
     1.1 --- a/src/ZF/ex/Term.thy	Thu Jan 28 10:21:45 1999 +0100
     1.2 +++ b/src/ZF/ex/Term.thy	Thu Jan 28 18:10:17 1999 +0100
     1.3 @@ -20,27 +20,24 @@
     1.4      type_intrs  "[list_univ RS subsetD]"
     1.5  *)
     1.6  
     1.7 -consts
     1.8 +constdefs
     1.9    term_rec  :: [i, [i,i,i]=>i] => i
    1.10 -  term_map  :: [i=>i, i] => i
    1.11 -  term_size :: i=>i
    1.12 -  reflect   :: i=>i
    1.13 -  preorder  :: i=>i
    1.14 -  postorder :: i=>i
    1.15 -
    1.16 -defs
    1.17 -  term_rec_def
    1.18     "term_rec(t,d) == 
    1.19 -   Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z. g`z, zs)), t))"
    1.20 +    Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z. g`z, zs)), t))"
    1.21  
    1.22 -  term_map_def  "term_map(f,t) == term_rec(t, %x zs rs. Apply(f(x), rs))"
    1.23 +  term_map  :: [i=>i, i] => i
    1.24 +    "term_map(f,t) == term_rec(t, %x zs rs. Apply(f(x), rs))"
    1.25  
    1.26 -  term_size_def "term_size(t) == term_rec(t, %x zs rs. succ(list_add(rs)))"
    1.27 +  term_size :: i=>i
    1.28 +   "term_size(t) == term_rec(t, %x zs rs. succ(list_add(rs)))"
    1.29  
    1.30 -  reflect_def   "reflect(t) == term_rec(t, %x zs rs. Apply(x, rev(rs)))"
    1.31 +  reflect   :: i=>i
    1.32 +    "reflect(t) == term_rec(t, %x zs rs. Apply(x, rev(rs)))"
    1.33  
    1.34 -  preorder_def  "preorder(t) == term_rec(t, %x zs rs. Cons(x, flat(rs)))"
    1.35 +  preorder  :: i=>i
    1.36 +    "preorder(t) == term_rec(t, %x zs rs. Cons(x, flat(rs)))"
    1.37  
    1.38 -  postorder_def "postorder(t) == term_rec(t, %x zs rs. flat(rs) @ [x])"
    1.39 +  postorder :: i=>i
    1.40 +    "postorder(t) == term_rec(t, %x zs rs. flat(rs) @ [x])"
    1.41  
    1.42  end