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