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);