src/ZF/Induct/Comb.thy

--- a/src/ZF/Induct/Comb.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/ZF/Induct/Comb.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Induct/Comb.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson
     Copyright   1994  University of Cambridge
 *)
@@ -39,7 +38,7 @@
   "p ---> q" == "<p,q> \<in> contract^*"
 
 syntax (xsymbols)
-  "comb.app"    :: "[i, i] => i"    	     (infixl "\<bullet>" 90)
+  "comb.app"    :: "[i, i] => i"             (infixl "\<bullet>" 90)
 
 inductive
   domains "contract" \<subseteq> "comb \<times> comb"