src/HOL/ex/Term.thy
changeset 1376 92f83b9d17e1
parent 1151 c820b3cc3df0
child 1476 608483c2122a
     1.1 --- a/src/HOL/ex/Term.thy	Thu Nov 30 12:58:44 1995 +0100
     1.2 +++ b/src/HOL/ex/Term.thy	Fri Dec 01 12:03:13 1995 +0100
     1.3 @@ -16,14 +16,14 @@
     1.4  arities term :: (term)term
     1.5  
     1.6  consts
     1.7 -  term		:: "'a item set => 'a item set"
     1.8 -  Rep_term	:: "'a term => 'a item"
     1.9 -  Abs_term	:: "'a item => 'a term"
    1.10 -  Rep_Tlist	:: "'a term list => 'a item"
    1.11 -  Abs_Tlist	:: "'a item => 'a term list"
    1.12 -  App		:: "['a, ('a term)list] => 'a term"
    1.13 -  Term_rec	:: "['a item, ['a item , 'a item, 'b list]=>'b] => 'b"
    1.14 -  term_rec	:: "['a term, ['a ,'a term list, 'b list]=>'b] => 'b"
    1.15 +  term		:: 'a item set => 'a item set
    1.16 +  Rep_term	:: 'a term => 'a item
    1.17 +  Abs_term	:: 'a item => 'a term
    1.18 +  Rep_Tlist	:: 'a term list => 'a item
    1.19 +  Abs_Tlist	:: 'a item => 'a term list
    1.20 +  App		:: ['a, ('a term)list] => 'a term
    1.21 +  Term_rec	:: ['a item, ['a item , 'a item, 'b list]=>'b] => 'b
    1.22 +  term_rec	:: ['a term, ['a ,'a term list, 'b list]=>'b] => 'b
    1.23  
    1.24  inductive "term(A)"
    1.25    intrs