src/HOL/ex/Simult.thy
changeset 1376 92f83b9d17e1
parent 1151 c820b3cc3df0
child 1381 57777949b2f8
     1.1 --- a/src/HOL/ex/Simult.thy	Thu Nov 30 12:58:44 1995 +0100
     1.2 +++ b/src/HOL/ex/Simult.thy	Fri Dec 01 12:03:13 1995 +0100
     1.3 @@ -21,16 +21,16 @@
     1.4  arities  tree,forest :: (term)term
     1.5  
     1.6  consts
     1.7 -  TF          :: "'a item set => 'a item set"
     1.8 -  FNIL        :: "'a item"
     1.9 -  TCONS,FCONS :: "['a item, 'a item] => 'a item"
    1.10 -  Rep_Tree    :: "'a tree => 'a item"
    1.11 -  Abs_Tree    :: "'a item => 'a tree"
    1.12 -  Rep_Forest  :: "'a forest => 'a item"
    1.13 -  Abs_Forest  :: "'a item => 'a forest"
    1.14 -  Tcons       :: "['a, 'a forest] => 'a tree"
    1.15 -  Fcons       :: "['a tree, 'a forest] => 'a forest"
    1.16 -  Fnil        :: "'a forest"
    1.17 +  TF          :: 'a item set => 'a item set
    1.18 +  FNIL        :: 'a item
    1.19 +  TCONS,FCONS :: ['a item, 'a item] => 'a item
    1.20 +  Rep_Tree    :: 'a tree => 'a item
    1.21 +  Abs_Tree    :: 'a item => 'a tree
    1.22 +  Rep_Forest  :: 'a forest => 'a item
    1.23 +  Abs_Forest  :: 'a item => 'a forest
    1.24 +  Tcons       :: ['a, 'a forest] => 'a tree
    1.25 +  Fcons       :: ['a tree, 'a forest] => 'a forest
    1.26 +  Fnil        :: 'a forest
    1.27    TF_rec      :: "['a item, ['a item , 'a item, 'b]=>'b,     
    1.28                   'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b"
    1.29    tree_rec    :: "['a tree, ['a, 'a forest, 'b]=>'b,