| changeset 3842 | b55686a7b22c |
| parent 2130 | 53b6e0bc8ccf |
| child 4089 | 96fba19bcbe2 |
--- a/src/HOL/Lex/Prefix.ML Fri Oct 10 18:37:49 1997 +0200 +++ b/src/HOL/Lex/Prefix.ML Fri Oct 10 19:02:28 1997 +0200 @@ -6,7 +6,7 @@ open Prefix; -val [maj,min] = goal Prefix.thy "[| Q([]); !! y ys. Q(y#ys) |] ==> ! l.Q(l)"; +val [maj,min] = goal Prefix.thy "[| Q([]); !! y ys. Q(y#ys) |] ==> ! l. Q(l)"; by (rtac allI 1); by (list.induct_tac "l" 1); by (rtac maj 1);