equal
deleted
inserted
replaced
1 (* Title: HOL/Lex/Prefix.thy |
1 (* Title: HOL/Lex/Prefix.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Richard Mayr & Tobias Nipkow |
3 Author: Richard Mayr & Tobias Nipkow |
4 Copyright 1995 TUM |
4 Copyright 1995 TUM |
5 *) |
5 *) |
6 |
|
7 (* Junk: *) |
|
8 val [maj,min] = goal Prefix.thy "[| Q([]); !! y ys. Q(y#ys) |] ==> ! l. Q(l)"; |
|
9 by (rtac allI 1); |
|
10 by (induct_tac "l" 1); |
|
11 by (rtac maj 1); |
|
12 by (rtac min 1); |
|
13 val list_cases = result(); |
|
14 |
6 |
15 (** <= is a partial order: **) |
7 (** <= is a partial order: **) |
16 |
8 |
17 Goalw [prefix_def] "xs <= (xs::'a list)"; |
9 Goalw [prefix_def] "xs <= (xs::'a list)"; |
18 by (Simp_tac 1); |
10 by (Simp_tac 1); |