src/ZF/UNITY/Comp.thy
changeset 32960 69916a850301
parent 24893 b8ef7afe3a6b
child 46823 57bf0cecb366
--- a/src/ZF/UNITY/Comp.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/ZF/UNITY/Comp.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      ZF/UNITY/Comp.thy
-    ID:         $Id$
     Author:     Sidi O Ehmety, Computer Laboratory
     Copyright   1998  University of Cambridge
 
@@ -47,7 +46,7 @@
 definition
   localize  :: "[i=>i, i] => i"  where
   "localize(f,F) == mk_program(Init(F), Acts(F),
-		       AllowedActs(F) Int (UN G:preserves(f). Acts(G)))"
+                       AllowedActs(F) Int (UN G:preserves(f). Acts(G)))"
 
   
 (*** component and strict_component relations ***)