author | haftmann |
Wed, 24 Nov 2010 19:15:00 +0100 | |
changeset 40688 | a961ec75fc29 |
parent 40687 | 1aa56a048dce |
child 40689 | 3a10ce7cd436 |
--- a/src/HOL/Quotient_Examples/FSet.thy Wed Nov 24 16:51:13 2010 +0100 +++ b/src/HOL/Quotient_Examples/FSet.thy Wed Nov 24 19:15:00 2010 +0100 @@ -25,7 +25,7 @@ unfolding reflp_def symp_def transp_def by auto -text {* Cset type *} +text {* The @{text fset} type *} quotient_type 'a fset = "'a list" / "list_eq"