# HG changeset patch
# User webertj
# Date 1093534137 -7200
# Node ID 065ce5385a0696c930f656ef6bc87f69c13e8ee1
# Parent  394fb9b8908b4de2f18f18573c5e40ee31c1a46f
comment modified

diff -r 394fb9b8908b -r 065ce5385a06 src/HOL/ex/Refute_Examples.thy
--- 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"