| changeset 4423 | a129b817b58a |
| parent 4089 | 96fba19bcbe2 |
| child 4643 | 1b40fcac5a09 |
--- a/src/HOL/Lex/Prefix.ML Tue Dec 16 15:17:26 1997 +0100 +++ b/src/HOL/Lex/Prefix.ML Tue Dec 16 17:58:03 1997 +0100 @@ -35,7 +35,7 @@ qed "prefix_Cons"; goalw Prefix.thy [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)"; -by(Simp_tac 1); +by (Simp_tac 1); by (Fast_tac 1); qed"Cons_prefix_Cons"; Addsimps [Cons_prefix_Cons];