src/HOL/Finite_Set.thy
changeset 19313 45c9fc22904b
parent 19279 48b527d0331b
child 19363 667b5ea637dd
     1.1 --- a/src/HOL/Finite_Set.thy	Tue Mar 21 15:38:53 2006 +0100
     1.2 +++ b/src/HOL/Finite_Set.thy	Wed Mar 22 11:14:58 2006 +0100
     1.3 @@ -13,10 +13,8 @@
     1.4  subsection {* Definition and basic properties *}
     1.5  
     1.6  consts Finites :: "'a set set"
     1.7 -syntax
     1.8 -  finite :: "'a set => bool"
     1.9 -translations
    1.10 -  "finite A" == "A : Finites"
    1.11 +abbreviation (output)
    1.12 +  "finite A = (A : Finites)"
    1.13  
    1.14  inductive Finites
    1.15    intros