src/HOLCF/Ssum.thy
changeset 32960 69916a850301
parent 31115 7d6416f0d1e0
child 33504 b4210cc3ac97
--- a/src/HOLCF/Ssum.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOLCF/Ssum.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -25,9 +25,9 @@
 by (rule typedef_chfin [OF type_definition_Ssum below_Ssum_def])
 
 syntax (xsymbols)
-  "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
+  "++"          :: "[type, type] => type"       ("(_ \<oplus>/ _)" [21, 20] 20)
 syntax (HTML output)
-  "++"		:: "[type, type] => type"	("(_ \<oplus>/ _)" [21, 20] 20)
+  "++"          :: "[type, type] => type"       ("(_ \<oplus>/ _)" [21, 20] 20)
 
 subsection {* Definitions of constructors *}