src/HOL/Subst/UTerm.thy
changeset 1374 5e407f2a3323
parent 1151 c820b3cc3df0
child 1381 57777949b2f8
     1.1 --- a/src/HOL/Subst/UTerm.thy	Wed Nov 29 16:58:30 1995 +0100
     1.2 +++ b/src/HOL/Subst/UTerm.thy	Wed Nov 29 17:01:41 1995 +0100
     1.3 @@ -14,15 +14,15 @@
     1.4    uterm     :: (term)term
     1.5  
     1.6  consts
     1.7 -  uterm     :: "'a item set => 'a item set"
     1.8 -  Rep_uterm :: "'a uterm => 'a item"
     1.9 -  Abs_uterm :: "'a item => 'a uterm"
    1.10 -  VAR       :: "'a item => 'a item"
    1.11 -  CONST     :: "'a item => 'a item"
    1.12 -  COMB      :: "['a item, 'a item] => 'a item"
    1.13 -  Var       :: "'a => 'a uterm"
    1.14 -  Const     :: "'a => 'a uterm"
    1.15 -  Comb      :: "['a uterm, 'a uterm] => 'a uterm"
    1.16 +  uterm     :: 'a item set => 'a item set
    1.17 +  Rep_uterm :: 'a uterm => 'a item
    1.18 +  Abs_uterm :: 'a item => 'a uterm
    1.19 +  VAR       :: 'a item => 'a item
    1.20 +  CONST     :: 'a item => 'a item
    1.21 +  COMB      :: ['a item, 'a item] => 'a item
    1.22 +  Var       :: 'a => 'a uterm
    1.23 +  Const     :: 'a => 'a uterm
    1.24 +  Comb      :: ['a uterm, 'a uterm] => 'a uterm
    1.25    UTerm_rec :: "['a item, 'a item => 'b, 'a item => 'b, 
    1.26                  ['a item , 'a item, 'b, 'b]=>'b] => 'b"
    1.27    uterm_rec :: "['a uterm, 'a => 'b, 'a => 'b,