equal
deleted
inserted
replaced
4 Copyright 1995 TUM |
4 Copyright 1995 TUM |
5 *) |
5 *) |
6 |
6 |
7 open Prefix; |
7 open Prefix; |
8 |
8 |
9 val [maj,min] = goal Prefix.thy "[| Q([]); !! y ys. Q(y#ys) |] ==> ! l.Q(l)"; |
9 val [maj,min] = goal Prefix.thy "[| Q([]); !! y ys. Q(y#ys) |] ==> ! l. Q(l)"; |
10 by (rtac allI 1); |
10 by (rtac allI 1); |
11 by (list.induct_tac "l" 1); |
11 by (list.induct_tac "l" 1); |
12 by (rtac maj 1); |
12 by (rtac maj 1); |
13 by (rtac min 1); |
13 by (rtac min 1); |
14 val list_cases = result(); |
14 val list_cases = result(); |