src/HOL/TLA/Stfun.ML
changeset 17309 c43ed29bd197
parent 12607 16b63730cfbb
--- a/src/HOL/TLA/Stfun.ML	Wed Sep 07 20:22:15 2005 +0200
+++ b/src/HOL/TLA/Stfun.ML	Wed Sep 07 20:22:39 2005 +0200
@@ -1,5 +1,6 @@
-(* 
-    File:	 Stfun.ML
+(*
+    File:        Stfun.ML
+    ID:          $Id$
     Author:      Stephan Merz
     Copyright:   1998 University of Munich
 
@@ -51,7 +52,7 @@
 
 Goal "!!v. basevars (v::bool stfun, v) ==> False";
 by (etac baseE 1);
-by (subgoal_tac "(LIFT (v,v)) x = (True, False)" 1); 
+by (subgoal_tac "(LIFT (v,v)) x = (True, False)" 1);
 by (atac 2);
 by (Asm_full_simp_tac 1);