src/HOL/Sexp.thy
changeset 1370 7361ac9b024d
parent 1151 c820b3cc3df0
child 1395 7095d6b89734
     1.1 --- a/src/HOL/Sexp.thy	Mon Nov 27 13:44:56 1995 +0100
     1.2 +++ b/src/HOL/Sexp.thy	Wed Nov 29 16:44:59 1995 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  Sexp = Univ +
     1.6  consts
     1.7 -  sexp      :: "'a item set"
     1.8 +  sexp      :: 'a item set
     1.9  
    1.10    sexp_case :: "['a=>'b, nat=>'b, ['a item, 'a item]=>'b, 
    1.11                  'a item] => 'b"