removed some more quotes
authorclasohm
Fri Dec 01 13:03:34 1995 +0100 (1995-12-01)
changeset 138157777949b2f8
parent 1380 2f8055af9c04
child 1382 7e97232c1159
removed some more quotes
src/HOL/Subst/UTLemmas.thy
src/HOL/Subst/UTerm.thy
src/HOL/ex/Simult.thy
     1.1 --- a/src/HOL/Subst/UTLemmas.thy	Fri Dec 01 12:27:09 1995 +0100
     1.2 +++ b/src/HOL/Subst/UTLemmas.thy	Fri Dec 01 13:03:34 1995 +0100
     1.3 @@ -9,8 +9,8 @@
     1.4  
     1.5  consts
     1.6  
     1.7 -  vars_of       ::   "'a uterm=>'a set"
     1.8 -  "<:"          ::   "['a uterm,'a uterm]=>bool"   (infixl 54) 
     1.9 +  vars_of       ::   'a uterm=>'a set
    1.10 +  "<:"          ::   ['a uterm,'a uterm]=>bool   (infixl 54) 
    1.11  
    1.12  rules  (*Definitions*)
    1.13  
     2.1 --- a/src/HOL/Subst/UTerm.thy	Fri Dec 01 12:27:09 1995 +0100
     2.2 +++ b/src/HOL/Subst/UTerm.thy	Fri Dec 01 13:03:34 1995 +0100
     2.3 @@ -23,10 +23,10 @@
     2.4    Var       :: 'a => 'a uterm
     2.5    Const     :: 'a => 'a uterm
     2.6    Comb      :: ['a uterm, 'a uterm] => 'a uterm
     2.7 -  UTerm_rec :: "['a item, 'a item => 'b, 'a item => 'b, 
     2.8 -                ['a item , 'a item, 'b, 'b]=>'b] => 'b"
     2.9 -  uterm_rec :: "['a uterm, 'a => 'b, 'a => 'b, 
    2.10 -                ['a uterm, 'a uterm,'b,'b]=>'b] => 'b"
    2.11 +  UTerm_rec :: ['a item, 'a item => 'b, 'a item => 'b, 
    2.12 +                ['a item , 'a item, 'b, 'b]=>'b] => 'b
    2.13 +  uterm_rec :: ['a uterm, 'a => 'b, 'a => 'b, 
    2.14 +                ['a uterm, 'a uterm,'b,'b]=>'b] => 'b
    2.15  
    2.16  defs
    2.17       (*defining the concrete constructors*)
     3.1 --- a/src/HOL/ex/Simult.thy	Fri Dec 01 12:27:09 1995 +0100
     3.2 +++ b/src/HOL/ex/Simult.thy	Fri Dec 01 13:03:34 1995 +0100
     3.3 @@ -31,12 +31,12 @@
     3.4    Tcons       :: ['a, 'a forest] => 'a tree
     3.5    Fcons       :: ['a tree, 'a forest] => 'a forest
     3.6    Fnil        :: 'a forest
     3.7 -  TF_rec      :: "['a item, ['a item , 'a item, 'b]=>'b,     
     3.8 -                 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b"
     3.9 -  tree_rec    :: "['a tree, ['a, 'a forest, 'b]=>'b,          
    3.10 -                 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
    3.11 -  forest_rec  :: "['a forest, ['a, 'a forest, 'b]=>'b,        
    3.12 -                  'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b"
    3.13 +  TF_rec      :: ['a item, ['a item , 'a item, 'b]=>'b,     
    3.14 +                 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b
    3.15 +  tree_rec    :: ['a tree, ['a, 'a forest, 'b]=>'b,          
    3.16 +                 'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b
    3.17 +  forest_rec  :: ['a forest, ['a, 'a forest, 'b]=>'b,        
    3.18 +                  'b, ['a tree, 'a forest, 'b, 'b]=>'b] => 'b
    3.19  
    3.20  defs
    3.21       (*the concrete constants*)