src/HOL/Set.thy
changeset 12338 de0f4a63baa5
parent 12257 e3f7d6fb55d7
child 12633 ad9277743664
     1.1 --- a/src/HOL/Set.thy	Sat Dec 01 18:51:46 2001 +0100
     1.2 +++ b/src/HOL/Set.thy	Sat Dec 01 18:52:32 2001 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4  global
     1.5  
     1.6  typedecl 'a set
     1.7 -arities set :: ("term") "term"
     1.8 +arities set :: (type) type
     1.9  
    1.10  consts
    1.11    "{}"          :: "'a set"                             ("{}")
    1.12 @@ -42,8 +42,8 @@
    1.13  
    1.14  local
    1.15  
    1.16 -instance set :: ("term") ord ..
    1.17 -instance set :: ("term") minus ..
    1.18 +instance set :: (type) ord ..
    1.19 +instance set :: (type) minus ..
    1.20  
    1.21  
    1.22  subsection {* Additional concrete syntax *}