| changeset 15161 | 065ce5385a06 |
| parent 14809 | eaa5d6987ba2 |
| child 15297 | 0aff5d912422 |
--- a/src/HOL/ex/Refute_Examples.thy Tue Aug 24 17:55:24 2004 +0200 +++ b/src/HOL/ex/Refute_Examples.thy Thu Aug 26 17:28:57 2004 +0200 @@ -455,8 +455,9 @@ subsection {* Subtypes (typedef), typedecl *} +text {* A completely unspecified non-empty subset of @{typ "'a"}: *} + typedef 'a myTdef = "insert (arbitrary::'a) (arbitrary::'a set)" - -- {* a completely unspecified non-empty subset of @{typ "'a"} *} by auto lemma "(x::'a myTdef) = y"